---

Step * of Lemma subsequence-converges

∀a:ℝ. ∀x,y:ℕ ⟶ ℝ.
  ((∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = x[m])) supposing N ≤ n) ⇒ lim n→∞.x[n] = a ⇒ lim n→∞.y[n] = a)
BY
{ (Auto THEN (All (Unfold `converges-to`)) THEN Auto THEN ((InstHyp [⌜k⌝] (-2))⋅ THENA Auto) THEN ExRepD) }

1
1. a : ℝ
2. x : ℕ ⟶ ℝ
3. y : ℕ ⟶ ℝ
4. N1 : ℕ
5. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (y[n] = x[m])) supposing N1 ≤ n
6. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k)))))})
7. k : ℕ+
8. N : ℕ
9. ∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k))))
⊢ ∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|y[n] - a| ≤ (r1/r(k)))))}

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mexists{}N:\mBbbN{}.  \mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  ((n  \mleq{}  m)  \mwedge{}  (y[n]  =  x[m]))  supposing  N  \mleq{}  n)
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  a
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  a)


By

---

Latex:
(Auto
  THEN  (All  (Unfold  `converges-to`))
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index