---

Step * of Lemma cantor_ivl-converges-ext

∀a,b:ℝ.  ∀f:ℕ ⟶ 𝔹. fst(cantor_ivl(a;b;f;n))↓ as n→∞ supposing a ≤ b
BY
{ Extract of Obid: cantor_ivl-converges
  not unfolding  divide cantor-interval cantor_cauchy
  finishing with (Reduce 0 THEN Auto THEN ProveStrict)
  normalizes to:
  
  λa,b,f. <λn.eval m = 4 * n in
              let x,y = cantor-interval(a;b;f;cantor_cauchy(a;b;m)) 
              in (x m) ÷ 4
          , λk.(cantor_cauchy(a;b;4 * k) + 1)
          > }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  fst(cantor\_ivl(a;b;f;n))\mdownarrow{}  as  n\mrightarrow{}\minfty{}  supposing  a  \mleq{}  b


By

---

Latex:
Extract  of  Obid:  cantor\_ivl-converges
not  unfolding    divide  cantor-interval  cantor\_cauchy
finishing  with  (Reduce  0  THEN  Auto  THEN  ProveStrict)
normalizes  to:

\mlambda{}a,b,f.  <\mlambda{}n.eval  m  =  4  *  n  in
                        let  x,y  =  cantor-interval(a;b;f;cantor\_cauchy(a;b;m)) 
                        in  (x  m)  \mdiv{}  4
                ,  \mlambda{}k.(cantor\_cauchy(a;b;4  *  k)  +  1)
                >

---

Home Index