---

Step * 1 1 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. y : ℕ ⟶ X
10. subsequence(a,b.a ≡ b;n.x n;n.y n)
11. mcauchy(d1;n.y n)
12. a : X
13. k : ℕ+
14. ∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (mdist(d2;x n;x m) ≤ (r1/r(2 * k)))))]
15. ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d1;y n;a) ≤ (r1/r(2 * k)))))]
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d2;x n;a) ≤ (r1/r(k)))))]
BY
{ (D -6 THEN D -2 THEN D -1) }

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. y : ℕ ⟶ X
10. N : ℕ
11. ∀n:ℕ. ∃n@0:ℕ. ((n ≤ n@0) ∧ y n ≡ x n@0) supposing N ≤ n
12. mcauchy(d1;n.y n)
13. a : X
14. k : ℕ+
15. N1 : ℕ
16. [%19] : ∀n,m:ℕ.  ((N1 ≤ n) ⇒ (N1 ≤ m) ⇒ (mdist(d2;x n;x m) ≤ (r1/r(2 * k))))
17. N2 : ℕ
18. [%21] : ∀n:ℕ. ((N2 ≤ n) ⇒ (mdist(d1;y n;a) ≤ (r1/r(2 * 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.  y  :  \mBbbN{}  {}\mrightarrow{}  X
10.  subsequence(a,b.a  \mequiv{}  b;n.x  n;n.y  n)
11.  mcauchy(d1;n.y  n)
12.  a  :  X
13.  k  :  \mBbbN{}\msupplus{}
14.  \mexists{}N:\mBbbN{}  [(\mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (mdist(d2;x  n;x  m)  \mleq{}  (r1/r(2  *  k)))))]
15.  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d1;y  n;a)  \mleq{}  (r1/r(2  *  k)))))]
\mvdash{}  \mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d2;x  n;a)  \mleq{}  (r1/r(k)))))]


By

---

Latex:
(D  -6  THEN  D  -2  THEN  D  -1)

---

Home Index