---

Step * of Lemma cantor-to-interval_wf1

∀a,b:ℝ.  ∀f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) ∈ {x:ℝ| lim n→∞.fst(cantor-interval(a;b;f;n)) = x} ) supposing a ≤ b
BY
{ (Auto THEN Unfold `cantor-to-interval` 0) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
⊢ λn.eval m = 4 * n in
     let x,y = cantor-interval(a;b;f;cantor_cauchy(a;b;m)) 
     in (x m) ÷ 4 ∈ {x:ℝ| lim n→∞.fst(cantor-interval(a;b;f;n)) = x} 

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (cantor-to-interval(a;b;f)  \mmember{}  \{x:\mBbbR{}|  lim  n\mrightarrow{}\minfty{}.fst(cantor-interval(a;b;f;n))  =  x\}  )  \000Csupposing  a  \mleq{}  b


By

---

Latex:
(Auto  THEN  Unfold  `cantor-to-interval`  0)

---

Home Index