---

Step * of Lemma cantor-interval-req

∀a,b:ℝ. ∀f:ℕ ⟶ 𝔹. ∀n:ℕ.
  (((fst(cantor-interval(a;b;f;n))) = (fst(cantor_ivl(a;b;f;n))))
  ∧ ((snd(cantor-interval(a;b;f;n))) = (snd(cantor_ivl(a;b;f;n)))))
BY
{ (InductionOnNat THENA Auto) }

1
.....basecase..... 
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
⊢ ((fst(cantor-interval(a;b;f;0))) = (fst(cantor_ivl(a;b;f;0))))
∧ ((snd(cantor-interval(a;b;f;0))) = (snd(cantor_ivl(a;b;f;0))))

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

---

Latex:

---

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


By

---

Latex:
(InductionOnNat  THENA  Auto)

---

Home Index