---

Step * of Lemma subsequence-mconverges-to

∀[X:Type]. ∀[d:metric(X)]. ∀[a:X].
  ∀x,y:ℕ ⟶ X.  (subsequence(a,b.a ≡ b;n.x[n];n.y[n]) ⇒ lim n→∞.x[n] = a ⇒ lim n→∞.y[n] = a)
BY
{ (Auto
   THEN (All (Unfolds ``mconverges-to subsequence``))
   THEN Auto
   THEN ((InstHyp [⌜k⌝] (-2))⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜imax(N;N1)⌝]⋅
   THEN Auto
   THEN FLemma `imax_lb` [-1]
   THEN Auto
   THEN (InstHyp [⌜n⌝] 7⋅ THEN Auto)
   THEN ExRepD) }

1
1. X : Type
2. d : metric(X)
3. a : X
4. x : ℕ ⟶ X
5. y : ℕ ⟶ X
6. N1 : ℕ
7. ∀n:ℕ. ∃n@0:ℕ. ((n ≤ n@0) ∧ y[n] ≡ x[n@0]) supposing N1 ≤ n
8. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x[n];a) ≤ (r1/r(k)))))])
9. k : ℕ+
10. N : ℕ
11. ∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x[n];a) ≤ (r1/r(k))))
12. n : ℕ
13. imax(N;N1) ≤ n
14. N ≤ n
15. N1 ≤ n
16. n@0 : ℕ
17. n ≤ n@0
18. y[n] ≡ x[n@0]
⊢ mdist(d;y[n];a) ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[a:X].
    \mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  X.    (subsequence(a,b.a  \mequiv{}  b;n.x[n];n.y[n])  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  a)


By

---

Latex:
(Auto
  THEN  (All  (Unfolds  ``mconverges-to  subsequence``))
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}imax(N;N1)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  FLemma  `imax\_lb`  [-1]
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  7\mcdot{}  THEN  Auto)
  THEN  ExRepD)

---

Home Index