HomeHome Intuitionistic Logic Explorer
Theorem List (p. 86 of 95)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8501-8600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremngtmnft 8501 An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006.)
(A * → (A = -∞ ↔ ¬ -∞ < A))
 
Theoremxrrebnd 8502 An extended real is real iff it is strictly bounded by infinities. (Contributed by NM, 2-Feb-2006.)
(A * → (A ℝ ↔ (-∞ < A A < +∞)))
 
Theoremxrre 8503 A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
(((A * B ℝ) (-∞ < A AB)) → A ℝ)
 
Theoremxrre2 8504 An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
(((A * B * 𝐶 *) (A < B B < 𝐶)) → B ℝ)
 
Theoremxrre3 8505 A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
(((A * B ℝ) (BA A < +∞)) → A ℝ)
 
Theoremge0gtmnf 8506 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * 0 ≤ A) → -∞ < A)
 
Theoremge0nemnf 8507 A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * 0 ≤ A) → A ≠ -∞)
 
Theoremxrrege0 8508 A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
(((A * B ℝ) (0 ≤ A AB)) → A ℝ)
 
Theoremz2ge 8509* There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
((𝑀 𝑁 ℤ) → 𝑘 ℤ (𝑀𝑘 𝑁𝑘))
 
Theoremxnegeq 8510 Equality of two extended numbers with -𝑒 in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(A = B → -𝑒A = -𝑒B)
 
Theoremxnegpnf 8511 Minus +∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
-𝑒+∞ = -∞
 
Theoremxnegmnf 8512 Minus -∞. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
-𝑒-∞ = +∞
 
Theoremrexneg 8513 Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
(A ℝ → -𝑒A = -A)
 
Theoremxneg0 8514 The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
-𝑒0 = 0
 
Theoremxnegcl 8515 Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → -𝑒A *)
 
Theoremxnegneg 8516 Extended real version of negneg 7057. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → -𝑒-𝑒A = A)
 
Theoremxneg11 8517 Extended real version of neg11 7058. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (-𝑒A = -𝑒BA = B))
 
Theoremxltnegi 8518 Forward direction of xltneg 8519. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B * A < B) → -𝑒B < -𝑒A)
 
Theoremxltneg 8519 Extended real version of ltneg 7252. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (A < B ↔ -𝑒B < -𝑒A))
 
Theoremxleneg 8520 Extended real version of leneg 7255. (Contributed by Mario Carneiro, 20-Aug-2015.)
((A * B *) → (AB ↔ -𝑒B ≤ -𝑒A))
 
Theoremxlt0neg1 8521 Extended real version of lt0neg1 7258. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → (A < 0 ↔ 0 < -𝑒A))
 
Theoremxlt0neg2 8522 Extended real version of lt0neg2 7259. (Contributed by Mario Carneiro, 20-Aug-2015.)
(A * → (0 < A ↔ -𝑒A < 0))
 
Theoremxle0neg1 8523 Extended real version of le0neg1 7260. (Contributed by Mario Carneiro, 9-Sep-2015.)
(A * → (A ≤ 0 ↔ 0 ≤ -𝑒A))
 
Theoremxle0neg2 8524 Extended real version of le0neg2 7261. (Contributed by Mario Carneiro, 9-Sep-2015.)
(A * → (0 ≤ A ↔ -𝑒A ≤ 0))
 
Theoremxnegcld 8525 Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
(φA *)       (φ → -𝑒A *)
 
Theoremxrex 8526 The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
* V
 
3.5.3  Real number intervals
 
Syntaxcioo 8527 Extend class notation with the set of open intervals of extended reals.
class (,)
 
Syntaxcioc 8528 Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
 
Syntaxcico 8529 Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
 
Syntaxcicc 8530 Extend class notation with the set of closed intervals of extended reals.
class [,]
 
Definitiondf-ioo 8531* Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,) = (x *, y * ↦ {z * ∣ (x < z z < y)})
 
Definitiondf-ioc 8532* Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
(,] = (x *, y * ↦ {z * ∣ (x < z zy)})
 
Definitiondf-ico 8533* Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,) = (x *, y * ↦ {z * ∣ (xz z < y)})
 
Definitiondf-icc 8534* Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
[,] = (x *, y * ↦ {z * ∣ (xz zy)})
 
Theoremixxval 8535* Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       ((A * B *) → (A𝑂B) = {z * ∣ (A𝑅z z𝑆B)})
 
Theoremelixx1 8536* Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       ((A * B *) → (𝐶 (A𝑂B) ↔ (𝐶 * A𝑅𝐶 𝐶𝑆B)))
 
Theoremixxf 8537* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       𝑂:(ℝ* × ℝ*)⟶𝒫 ℝ*
 
Theoremixxex 8538* The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       𝑂 V
 
Theoremixxssxr 8539* The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       (A𝑂B) ⊆ ℝ*
 
Theoremelixx3g 8540* Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A * and B *. (Contributed by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})       (𝐶 (A𝑂B) ↔ ((A * B * 𝐶 *) (A𝑅𝐶 𝐶𝑆B)))
 
Theoremixxssixx 8541* An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})    &   𝑃 = (x *, y * ↦ {z * ∣ (x𝑇z z𝑈y)})    &   ((A * w *) → (A𝑅wA𝑇w))    &   ((w * B *) → (w𝑆Bw𝑈B))       (A𝑂B) ⊆ (A𝑃B)
 
Theoremixxdisj 8542* Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})    &   𝑃 = (x *, y * ↦ {z * ∣ (x𝑇z z𝑈y)})    &   ((B * w *) → (B𝑇w ↔ ¬ w𝑆B))       ((A * B * 𝐶 *) → ((A𝑂B) ∩ (B𝑃𝐶)) = ∅)
 
Theoremixxss1 8543* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})    &   𝑃 = (x *, y * ↦ {z * ∣ (x𝑇z z𝑆y)})    &   ((A * B * w *) → ((A𝑊B B𝑇w) → A𝑅w))       ((A * A𝑊B) → (B𝑃𝐶) ⊆ (A𝑂𝐶))
 
Theoremixxss2 8544* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})    &   𝑃 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑇y)})    &   ((w * B * 𝐶 *) → ((w𝑇B B𝑊𝐶) → w𝑆𝐶))       ((𝐶 * B𝑊𝐶) → (A𝑃B) ⊆ (A𝑂𝐶))
 
Theoremixxss12 8545* Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
𝑂 = (x *, y * ↦ {z * ∣ (x𝑅z z𝑆y)})    &   𝑃 = (x *, y * ↦ {z * ∣ (x𝑇z z𝑈y)})    &   ((A * 𝐶 * w *) → ((A𝑊𝐶 𝐶𝑇w) → A𝑅w))    &   ((w * 𝐷 * B *) → ((w𝑈𝐷 𝐷𝑋B) → w𝑆B))       (((A * B *) (A𝑊𝐶 𝐷𝑋B)) → (𝐶𝑃𝐷) ⊆ (A𝑂B))
 
Theoremiooex 8546 The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
(,) V
 
Theoremiooval 8547* Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (A(,)B) = {x * ∣ (A < x x < B)})
 
Theoremiooidg 8548 An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
(A * → (A(,)A) = ∅)
 
Theoremelioo3g 8549 Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A * and B *. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
(𝐶 (A(,)B) ↔ ((A * B * 𝐶 *) (A < 𝐶 𝐶 < B)))
 
Theoremelioo1 8550 Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (𝐶 (A(,)B) ↔ (𝐶 * A < 𝐶 𝐶 < B)))
 
Theoremelioore 8551 A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
(A (B(,)𝐶) → A ℝ)
 
Theoremlbioog 8552 An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → ¬ A (A(,)B))
 
Theoremubioog 8553 An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → ¬ B (A(,)B))
 
Theoremiooval2 8554* Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (A(,)B) = {x ℝ ∣ (A < x x < B)})
 
Theoremiooss1 8555 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
((A * AB) → (B(,)𝐶) ⊆ (A(,)𝐶))
 
Theoremiooss2 8556 Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
((𝐶 * B𝐶) → (A(,)B) ⊆ (A(,)𝐶))
 
Theoremiocval 8557* Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (A(,]B) = {x * ∣ (A < x xB)})
 
Theoremicoval 8558* Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (A[,)B) = {x * ∣ (Ax x < B)})
 
Theoremiccval 8559* Value of the closed interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (A[,]B) = {x * ∣ (Ax xB)})
 
Theoremelioo2 8560 Membership in an open interval of extended reals. (Contributed by NM, 6-Feb-2007.)
((A * B *) → (𝐶 (A(,)B) ↔ (𝐶 A < 𝐶 𝐶 < B)))
 
Theoremelioc1 8561 Membership in an open-below, closed-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (𝐶 (A(,]B) ↔ (𝐶 * A < 𝐶 𝐶B)))
 
Theoremelico1 8562 Membership in a closed-below, open-above interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (𝐶 (A[,)B) ↔ (𝐶 * A𝐶 𝐶 < B)))
 
Theoremelicc1 8563 Membership in a closed interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
((A * B *) → (𝐶 (A[,]B) ↔ (𝐶 * A𝐶 𝐶B)))
 
Theoremiccid 8564 A closed interval with identical lower and upper bounds is a singleton. (Contributed by Jeff Hankins, 13-Jul-2009.)
(A * → (A[,]A) = {A})
 
Theoremicc0r 8565 An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.)
((A * B *) → (B < A → (A[,]B) = ∅))
 
Theoremeliooxr 8566 An inhabited open interval spans an interval of extended reals. (Contributed by NM, 17-Aug-2008.)
(A (B(,)𝐶) → (B * 𝐶 *))
 
Theoremeliooord 8567 Ordering implied by a member of an open interval of reals. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 9-May-2014.)
(A (B(,)𝐶) → (B < A A < 𝐶))
 
Theoremubioc1 8568 The upper bound belongs to an open-below, closed-above interval. See ubicc2 8623. (Contributed by FL, 29-May-2014.)
((A * B * A < B) → B (A(,]B))
 
Theoremlbico1 8569 The lower bound belongs to a closed-below, open-above interval. See lbicc2 8622. (Contributed by FL, 29-May-2014.)
((A * B * A < B) → A (A[,)B))
 
Theoremiccleub 8570 An element of a closed interval is less than or equal to its upper bound. (Contributed by Jeff Hankins, 14-Jul-2009.)
((A * B * 𝐶 (A[,]B)) → 𝐶B)
 
Theoremiccgelb 8571 An element of a closed interval is more than or equal to its lower bound (Contributed by Thierry Arnoux, 23-Dec-2016.)
((A * B * 𝐶 (A[,]B)) → A𝐶)
 
Theoremelioo5 8572 Membership in an open interval of extended reals. (Contributed by NM, 17-Aug-2008.)
((A * B * 𝐶 *) → (𝐶 (A(,)B) ↔ (A < 𝐶 𝐶 < B)))
 
Theoremelioo4g 8573 Membership in an open interval of extended reals. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐶 (A(,)B) ↔ ((A * B * 𝐶 ℝ) (A < 𝐶 𝐶 < B)))
 
Theoremioossre 8574 An open interval is a set of reals. (Contributed by NM, 31-May-2007.)
(A(,)B) ⊆ ℝ
 
Theoremelioc2 8575 Membership in an open-below, closed-above real interval. (Contributed by Paul Chapman, 30-Dec-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
((A * B ℝ) → (𝐶 (A(,]B) ↔ (𝐶 A < 𝐶 𝐶B)))
 
Theoremelico2 8576 Membership in a closed-below, open-above real interval. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 14-Jun-2014.)
((A B *) → (𝐶 (A[,)B) ↔ (𝐶 A𝐶 𝐶 < B)))
 
Theoremelicc2 8577 Membership in a closed real interval. (Contributed by Paul Chapman, 21-Sep-2007.) (Revised by Mario Carneiro, 14-Jun-2014.)
((A B ℝ) → (𝐶 (A[,]B) ↔ (𝐶 A𝐶 𝐶B)))
 
Theoremelicc2i 8578 Inference for membership in a closed interval. (Contributed by Scott Fenton, 3-Jun-2013.)
A     &   B        (𝐶 (A[,]B) ↔ (𝐶 A𝐶 𝐶B))
 
Theoremelicc4 8579 Membership in a closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014.) (Proof shortened by Mario Carneiro, 1-Jan-2017.)
((A * B * 𝐶 *) → (𝐶 (A[,]B) ↔ (A𝐶 𝐶B)))
 
Theoremiccss 8580 Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 20-Feb-2015.)
(((A B ℝ) (A𝐶 𝐷B)) → (𝐶[,]𝐷) ⊆ (A[,]B))
 
Theoremiccssioo 8581 Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
(((A * B *) (A < 𝐶 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A(,)B))
 
Theoremicossico 8582 Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Thierry Arnoux, 21-Sep-2017.)
(((A * B *) (A𝐶 𝐷B)) → (𝐶[,)𝐷) ⊆ (A[,)B))
 
Theoremiccss2 8583 Condition for a closed interval to be a subset of another closed interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Apr-2015.)
((𝐶 (A[,]B) 𝐷 (A[,]B)) → (𝐶[,]𝐷) ⊆ (A[,]B))
 
Theoremiccssico 8584 Condition for a closed interval to be a subset of a half-open interval. (Contributed by Mario Carneiro, 9-Sep-2015.)
(((A * B *) (A𝐶 𝐷 < B)) → (𝐶[,]𝐷) ⊆ (A[,)B))
 
Theoremiccssioo2 8585 Condition for a closed interval to be a subset of an open interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
((𝐶 (A(,)B) 𝐷 (A(,)B)) → (𝐶[,]𝐷) ⊆ (A(,)B))
 
Theoremiccssico2 8586 Condition for a closed interval to be a subset of a closed-below, open-above interval. (Contributed by Mario Carneiro, 20-Feb-2015.)
((𝐶 (A[,)B) 𝐷 (A[,)B)) → (𝐶[,]𝐷) ⊆ (A[,)B))
 
Theoremioomax 8587 The open interval from minus to plus infinity. (Contributed by NM, 6-Feb-2007.)
(-∞(,)+∞) = ℝ
 
Theoremiccmax 8588 The closed interval from minus to plus infinity. (Contributed by Mario Carneiro, 4-Jul-2014.)
(-∞[,]+∞) = ℝ*
 
Theoremioopos 8589 The set of positive reals expressed as an open interval. (Contributed by NM, 7-May-2007.)
(0(,)+∞) = {x ℝ ∣ 0 < x}
 
Theoremioorp 8590 The set of positive reals expressed as an open interval. (Contributed by Steve Rodriguez, 25-Nov-2007.)
(0(,)+∞) = ℝ+
 
Theoremiooshf 8591 Shift the arguments of the open interval function. (Contributed by NM, 17-Aug-2008.)
(((A B ℝ) (𝐶 𝐷 ℝ)) → ((AB) (𝐶(,)𝐷) ↔ A ((𝐶 + B)(,)(𝐷 + B))))
 
Theoremiocssre 8592 A closed-above interval with real upper bound is a set of reals. (Contributed by FL, 29-May-2014.)
((A * B ℝ) → (A(,]B) ⊆ ℝ)
 
Theoremicossre 8593 A closed-below interval with real lower bound is a set of reals. (Contributed by Mario Carneiro, 14-Jun-2014.)
((A B *) → (A[,)B) ⊆ ℝ)
 
Theoremiccssre 8594 A closed real interval is a set of reals. (Contributed by FL, 6-Jun-2007.) (Proof shortened by Paul Chapman, 21-Jan-2008.)
((A B ℝ) → (A[,]B) ⊆ ℝ)
 
Theoremiccssxr 8595 A closed interval is a set of extended reals. (Contributed by FL, 28-Jul-2008.) (Revised by Mario Carneiro, 4-Jul-2014.)
(A[,]B) ⊆ ℝ*
 
Theoremiocssxr 8596 An open-below, closed-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
(A(,]B) ⊆ ℝ*
 
Theoremicossxr 8597 A closed-below, open-above interval is a subset of the extended reals. (Contributed by FL, 29-May-2014.) (Revised by Mario Carneiro, 4-Jul-2014.)
(A[,)B) ⊆ ℝ*
 
Theoremioossicc 8598 An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.)
(A(,)B) ⊆ (A[,]B)
 
Theoremicossicc 8599 A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016.)
(A[,)B) ⊆ (A[,]B)
 
Theoremiocssicc 8600 A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017.)
(A(,]B) ⊆ (A[,]B)
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9457
  Copyright terms: Public domain < Previous  Next >