---

Step * of Lemma converges-cauchy-witness

∀[x:ℕ ⟶ ℝ]. ∀[y:ℝ]. ∀[cvg:lim n→∞.x[n] = y].  (λk.(cvg (2 * k)) ∈ cauchy(n.x[n]))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN (Assert <y, cvg> ∈ x[n]↓ as n→∞ BY Auto)) }

1
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])

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[y:\mBbbR{}].  \mforall{}[cvg:lim  n\mrightarrow{}\minfty{}.x[n]  =  y].    (\mlambda{}k.(cvg  (2  *  k))  \mmember{}  cauchy(n.x[n]))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  (Assert  <y,  cvg>  \mmember{}  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  BY  Auto))

---

Home Index