---

Step * of Lemma converges-iff-cauchy-ext

∀x:ℕ ⟶ ℝ. (x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n]))
BY
{ Extract of Obid: converges-iff-cauchy
  not unfolding  divide
  finishing with (RepUR ``accelerate`` 0 THEN Auto)
  normalizes to:
  
  λx.<λconverges.let y,c = converges 
                 in λk.(c (2 * k))
     , λcauchy.<accelerate(2;λn.(x (cauchy n) n)), λk.((cauchy (4 * k)) + 1)>
     > }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  (x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  \mLeftarrow{}{}\mRightarrow{}  cauchy(n.x[n]))


By

---

Latex:
Extract  of  Obid:  converges-iff-cauchy
not  unfolding    divide
finishing  with  (RepUR  ``accelerate``  0  THEN  Auto)
normalizes  to:

\mlambda{}x.<\mlambda{}converges.let  y,c  =  converges 
                              in  \mlambda{}k.(c  (2  *  k))
      ,  \mlambda{}cauchy.<accelerate(2;\mlambda{}n.(x  (cauchy  n)  n)),  \mlambda{}k.((cauchy  (4  *  k))  +  1)>
      >

---

Home Index