---

Step * of Lemma i-finite-iff-bounded

∀I:Interval. (i-finite(I) ⇐⇒ ∃a,b:ℝ. ∀[r:ℝ]. a≤r≤b supposing r ∈ I)
BY
{ Auto }

1
1. I : Interval
2. i-finite(I)
⊢ ∃a,b:ℝ. ∀[r:ℝ]. a≤r≤b supposing r ∈ I

2
1. I : Interval
2. ∃a,b:ℝ. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
⊢ i-finite(I)

---

Latex:

---

Latex:
\mforall{}I:Interval.  (i-finite(I)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a,b:\mBbbR{}.  \mforall{}[r:\mBbbR{}].  a\mleq{}r\mleq{}b  supposing  r  \mmember{}  I)


By

---

Latex:
Auto

---

Home Index