---

Step * of Lemma metric-leq-converges-to

∀[X:Type]. ∀[d1,d2:metric(X)].  (d2 ≤ d1 ⇒ (∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x[n] = y ⇒ lim n→∞.x[n] = y)))
BY
{ (RepUR ``metric-leq`` 0 THEN Auto THEN RepeatFor 5 (ParallelLast)) }

1
1. X : Type
2. d1 : metric(X)
3. d2 : metric(X)
4. ∀x,y:X.  (mdist(d2;x;y) ≤ mdist(d1;x;y))
5. x : ℕ ⟶ X
6. y : X
7. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d1;x[n];y) ≤ (r1/r(k)))))])
8. k : ℕ+
9. N : ℕ
10. ∀n:ℕ. ((N ≤ n) ⇒ (mdist(d1;x[n];y) ≤ (r1/r(k))))
11. n : ℕ
12. N ≤ n
13. mdist(d1;x[n];y) ≤ (r1/r(k))
⊢ mdist(d2;x[n];y) ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d1,d2:metric(X)].
    (d2  \mleq{}  d1  {}\mRightarrow{}  (\mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  \mforall{}y:X.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  y  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  y)))


By

---

Latex:
(RepUR  ``metric-leq``  0  THEN  Auto  THEN  RepeatFor  5  (ParallelLast))

---

Home Index