---

Step * 1 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. 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)))))]
BY
{ ((Assert ∃M:ℕ. ((N ≤ M) ∧ (N1 ≤ M) ∧ (N2 ≤ M)) BY
          (D 0 With ⌜imax(N;imax(N1;N2))⌝  THEN Auto))
   THEN ParallelLast
   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. 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. ∀n,m:ℕ.  ((N1 ≤ n) ⇒ (N1 ≤ m) ⇒ (mdist(d2;x n;x m) ≤ (r1/r(2 * k))))
17. N2 : ℕ
18. ∀n:ℕ. ((N2 ≤ n) ⇒ (mdist(d1;y n;a) ≤ (r1/r(2 * k))))
19. M : ℕ
20. N ≤ M
21. N1 ≤ M
22. N2 ≤ M
23. n : ℕ
24. M ≤ 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.  N  :  \mBbbN{}
11.  \mforall{}n:\mBbbN{}.  \mexists{}n@0:\mBbbN{}.  ((n  \mleq{}  n@0)  \mwedge{}  y  n  \mequiv{}  x  n@0)  supposing  N  \mleq{}  n
12.  mcauchy(d1;n.y  n)
13.  a  :  X
14.  k  :  \mBbbN{}\msupplus{}
15.  N1  :  \mBbbN{}
16.  [\%19]  :  \mforall{}n,m:\mBbbN{}.    ((N1  \mleq{}  n)  {}\mRightarrow{}  (N1  \mleq{}  m)  {}\mRightarrow{}  (mdist(d2;x  n;x  m)  \mleq{}  (r1/r(2  *  k))))
17.  N2  :  \mBbbN{}
18.  [\%21]  :  \mforall{}n:\mBbbN{}.  ((N2  \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:
((Assert  \mexists{}M:\mBbbN{}.  ((N  \mleq{}  M)  \mwedge{}  (N1  \mleq{}  M)  \mwedge{}  (N2  \mleq{}  M))  BY
                (D  0  With  \mkleeneopen{}imax(N;imax(N1;N2))\mkleeneclose{}    THEN  Auto))
  THEN  ParallelLast
  THEN  Auto)

---

Home Index