---

Step * of Lemma cantor-interval-rleq

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

1
.....basecase..... 
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. n : ℤ
⊢ ∀[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. 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{}].
    \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}].    ((fst(cantor-interval(a;b;f;n)))  \mleq{}  (snd(cantor-interval(a;b;f;n)))) 
    supposing  a  \mleq{}  b


By

---

Latex:
InductionOnNat

---

Home Index