---

Step * of Lemma cauchy-limit_wf

∀[x:ℕ ⟶ ℝ]. ∀[c:cauchy(n.x[n])].  (cauchy-limit(n.x[n];c) ∈ ℝ)
BY
{ ((RepeatFor 2 ((D 0 THENA Auto)) THEN RepUR ``cauchy-limit so_apply`` 0)
   THEN (Assert TERMOF{converges-iff-cauchy-ext:o, \\v:l} x ∈ x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n]) BY
               (GenConclAtAddr [2;1] THEN Unfold `all` -2 THEN All (RepUR ``so_apply``) THEN Auto))
   THEN RW (AddrC [2] (TagC (mk_tag_term 1))) (-1)) }

1
1. x : ℕ ⟶ ℝ
2. c : cauchy(n.x[n])
3. (λx.<λconverges.let y,c = converges 
                   in λk.(c (2 * k))
       , λcauchy.<accelerate(2;λn.(x (cauchy n) n)), λk.((cauchy (4 * k)) + 1)>
       >) 
   x ∈ x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n])
⊢ accelerate(2;λn.(x (c n) n)) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[c:cauchy(n.x[n])].    (cauchy-limit(n.x[n];c)  \mmember{}  \mBbbR{})


By

---

Latex:
((RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepUR  ``cauchy-limit  so\_apply``  0)
  THEN  (Assert  TERMOF\{converges-iff-cauchy-ext:o,  \mbackslash{}\mbackslash{}v:l\}  x  \mmember{}  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  \mLeftarrow{}{}\mRightarrow{}  cauchy(n.x[n])  BY
                          (GenConclAtAddr  [2;1]  THEN  Unfold  `all`  -2  THEN  All  (RepUR  ``so\_apply``)  THEN  Auto))
  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  1)))  (-1))

---

Home Index