---

Step * of Lemma req-from-converges

∀[x:ℕ ⟶ ℝ]. ∀[y:ℝ]. ∀[cvg:lim n→∞.x[n] = y].  (y = cauchy-limit(n.x[n];λk.(cvg (2 * k))))
BY
{ (InstLemma `converges-cauchy-witness` [] THEN RepeatFor 3 (ParallelLast') THEN Unhide THEN Auto) }

1
1. x : ℕ ⟶ ℝ
2. y : ℝ
3. cvg : lim n→∞.x[n] = y
4. λk.(cvg (2 * k)) ∈ cauchy(n.x[n])
⊢ y = cauchy-limit(n.x[n];λk.(cvg (2 * k)))

---

Latex:

---

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


By

---

Latex:
(InstLemma  `converges-cauchy-witness`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Unhide  THEN  Auto)

---

Home Index