---

Step * of Lemma cantor-interval-rless

∀a,b:ℝ.  ((a < b) ⇒ (∀n:ℕ. ∀f:ℕn ⟶ 𝔹.  ((fst(cantor-interval(a;b;f;n))) < (snd(cantor-interval(a;b;f;n))))))
BY
{ InductionOnNat }

1
.....basecase..... 
1. a : ℝ
2. b : ℝ
3. a < b
⊢ ∀f:ℕ0 ⟶ 𝔹. ((fst(cantor-interval(a;b;f;0))) < (snd(cantor-interval(a;b;f;0))))

2
.....upcase..... 
1. a : ℝ
2. b : ℝ
3. a < b
4. n : ℤ
5. [%2] : 0 < n
6. ∀f:ℕn - 1 ⟶ 𝔹. ((fst(cantor-interval(a;b;f;n - 1))) < (snd(cantor-interval(a;b;f;n - 1))))
⊢ ∀f:ℕn ⟶ 𝔹. ((fst(cantor-interval(a;b;f;n))) < (snd(cantor-interval(a;b;f;n))))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    ((a  <  b)
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    ((fst(cantor-interval(a;b;f;n)))  <  (snd(cantor-interval(a;b;f;n))))))


By

---

Latex:
InductionOnNat

---

Home Index