---

Step * 1 1 of Lemma metric-leq-complete


1. [X] : Type
2. [d1] : metric(X)
3. [d2] : metric(X)
4. d2 ≤ d1
5. ∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x[n] = y ⇒ lim n→∞.x[n] = y)
6. ∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ (∃y:ℕ ⟶ X. (subsequence(a,b.a ≡ b;n.x n;n.y n) ∧ mcauchy(d1;n.y n))))
7. ∀x:ℕ ⟶ X. (mcauchy(d1;n.x n) ⇒ x n↓ as n→∞)
8. x : ℕ ⟶ X
9. mcauchy(d2;n.x n)
10. y : ℕ ⟶ X
11. subsequence(a,b.a ≡ b;n.x n;n.y n)
12. mcauchy(d1;n.y n)
13. a : X
14. lim n→∞.y n = a
⊢ lim n→∞.x n = a
BY
{ (D 0 THEN Auto) }

1
1. [X] : Type
2. [d1] : metric(X)
3. [d2] : metric(X)
4. d2 ≤ d1
5. ∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x[n] = y ⇒ lim n→∞.x[n] = y)
6. ∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ (∃y:ℕ ⟶ X. (subsequence(a,b.a ≡ b;n.x n;n.y n) ∧ mcauchy(d1;n.y n))))
7. ∀x:ℕ ⟶ X. (mcauchy(d1;n.x n) ⇒ x n↓ as n→∞)
8. x : ℕ ⟶ X
9. mcauchy(d2;n.x n)
10. y : ℕ ⟶ X
11. subsequence(a,b.a ≡ b;n.x n;n.y n)
12. mcauchy(d1;n.y n)
13. a : X
14. lim n→∞.y n = a
15. k : ℕ+
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d2;x n;a) ≤ (r1/r(k)))))]

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d1]  :  metric(X)
3.  [d2]  :  metric(X)
4.  d2  \mleq{}  d1
5.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  \mforall{}y:X.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  y  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  y)
6.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X
          (mcauchy(d2;n.x  n)  {}\mRightarrow{}  (\mexists{}y:\mBbbN{}  {}\mrightarrow{}  X.  (subsequence(a,b.a  \mequiv{}  b;n.x  n;n.y  n)  \mwedge{}  mcauchy(d1;n.y  n))))
7.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d1;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
8.  x  :  \mBbbN{}  {}\mrightarrow{}  X
9.  mcauchy(d2;n.x  n)
10.  y  :  \mBbbN{}  {}\mrightarrow{}  X
11.  subsequence(a,b.a  \mequiv{}  b;n.x  n;n.y  n)
12.  mcauchy(d1;n.y  n)
13.  a  :  X
14.  lim  n\mrightarrow{}\minfty{}.y  n  =  a
\mvdash{}  lim  n\mrightarrow{}\minfty{}.x  n  =  a


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index