---

Step * 1 of Lemma subsequence-mconverges-to


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))
BY
{ ((Assert mdist(d;y[n];a) = mdist(d;x[n@0];a) BY
          (BLemma `mdist_functionality` THEN Auto))
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  a  :  X
4.  x  :  \mBbbN{}  {}\mrightarrow{}  X
5.  y  :  \mBbbN{}  {}\mrightarrow{}  X
6.  N1  :  \mBbbN{}
7.  \mforall{}n:\mBbbN{}.  \mexists{}n@0:\mBbbN{}.  ((n  \mleq{}  n@0)  \mwedge{}  y[n]  \mequiv{}  x[n@0])  supposing  N1  \mleq{}  n
8.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d;x[n];a)  \mleq{}  (r1/r(k)))))])
9.  k  :  \mBbbN{}\msupplus{}
10.  N  :  \mBbbN{}
11.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d;x[n];a)  \mleq{}  (r1/r(k))))
12.  n  :  \mBbbN{}
13.  imax(N;N1)  \mleq{}  n
14.  N  \mleq{}  n
15.  N1  \mleq{}  n
16.  n@0  :  \mBbbN{}
17.  n  \mleq{}  n@0
18.  y[n]  \mequiv{}  x[n@0]
\mvdash{}  mdist(d;y[n];a)  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  mdist(d;y[n];a)  =  mdist(d;x[n@0];a)  BY
                (BLemma  `mdist\_functionality`  THEN  Auto))
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index