---

Step * 1 of Lemma converges-cauchy-witness


1. x : ℕ ⟶ ℝ
2. y : ℝ
3. cvg : lim n→∞.x[n] = y
4. <y, cvg> ∈ x[n]↓ as n→∞
⊢ λk.(cvg (2 * k)) ∈ cauchy(n.x[n])
BY
{ ((Assert fst((TERMOF{converges-iff-cauchy-ext:o, \\v:l} x)) ∈ x[n]↓ as n→∞ ⇒ cauchy(n.x[n]) BY
          (GenConclAtAddr [2;1;1] THEN Unfold `all` -2 THEN All (RepUR ``so_apply``) THEN Auto))
   THEN RW (AddrC [2] (TagC (mk_tag_term 10))) (-1)
   ) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  y  :  \mBbbR{}
3.  cvg  :  lim  n\mrightarrow{}\minfty{}.x[n]  =  y
4.  <y,  cvg>  \mmember{}  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}
\mvdash{}  \mlambda{}k.(cvg  (2  *  k))  \mmember{}  cauchy(n.x[n])


By

---

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

---

Home Index