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