---

Step * 2 of Lemma i-finite-iff-bounded


1. I : Interval
2. ∃a,b:ℝ. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
⊢ i-finite(I)
BY
{ (ExRepD THEN Assert ⌜(¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))⌝⋅) }

1
.....assertion..... 
1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
⊢ (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))

2
1. I : Interval
2. a : ℝ
3. b : ℝ
4. ∀[r:ℝ]. a≤r≤b supposing r ∈ I
5. (¬((b + r1) ≤ b)) ∧ (¬(a ≤ (a - r1)))
⊢ i-finite(I)

---

Latex:

---

Latex:

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


By

---

Latex:
(ExRepD  THEN  Assert  \mkleeneopen{}(\mneg{}((b  +  r1)  \mleq{}  b))  \mwedge{}  (\mneg{}(a  \mleq{}  (a  -  r1)))\mkleeneclose{}\mcdot{})

---

Home Index