---

Step * of Lemma cantor-interval-cauchy-ext

∀a,b:ℝ.  ∀[f:ℕ ⟶ 𝔹]. cauchy(n.fst(cantor-interval(a;b;f;n))) supposing a ≤ b
BY
{ Extract of Obid: cantor-interval-cauchy
  not unfolding  divide log cbv_list_accum cantor_cauchy
  finishing with ((RepUR ``reg-seq-list-add`` 0 THEN RepeatFor 3 ((RecUnfold `cbv_list_accum` 0 THEN Reduce 0)))
                  THEN Try ((Fold `cantor_cauchy` 0 THEN Auto))
                  )
  normalizes to:
  
  λa,b,k. cantor_cauchy(a;b;k) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  cauchy(n.fst(cantor-interval(a;b;f;n)))  supposing  a  \mleq{}  b


By

---

Latex:
Extract  of  Obid:  cantor-interval-cauchy
not  unfolding    divide  log  cbv\_list\_accum  cantor\_cauchy
finishing  with  ((RepUR  ``reg-seq-list-add``  0
                                  THEN  RepeatFor  3  ((RecUnfold  `cbv\_list\_accum`  0  THEN  Reduce  0))
                                  )
                                THEN  Try  ((Fold  `cantor\_cauchy`  0  THEN  Auto))
                                )
normalizes  to:

\mlambda{}a,b,k.  cantor\_cauchy(a;b;k)

---

Home Index