---

Step * 1 1 1 1 1 1 2 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. ∀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
25. mdist(d1;y n;a) ≤ (r1/r(2 * k))
26. mdist(d2;x n;y n) ≤ (r1/r(2 * k))
⊢ mdist(d2;x n;a) ≤ (r1/r(k))
BY
{ ((Assert mdist(d2;y n;a) ≤ mdist(d1;y n;a) BY
          (BackThruHyp' 4 THEN Auto))
   THEN (Assert mdist(d2;y n;a) ≤ (r1/r(2 * k)) BY
               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
25. mdist(d1;y n;a) ≤ (r1/r(2 * k))
26. mdist(d2;x n;y n) ≤ (r1/r(2 * k))
27. mdist(d2;y n;a) ≤ mdist(d1;y n;a)
28. mdist(d2;y n;a) ≤ (r1/r(2 * k))
⊢ 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.  \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.  \mforall{}n:\mBbbN{}.  ((N2  \mleq{}  n)  {}\mRightarrow{}  (mdist(d1;y  n;a)  \mleq{}  (r1/r(2  *  k))))
19.  M  :  \mBbbN{}
20.  N  \mleq{}  M
21.  N1  \mleq{}  M
22.  N2  \mleq{}  M
23.  n  :  \mBbbN{}
24.  M  \mleq{}  n
25.  mdist(d1;y  n;a)  \mleq{}  (r1/r(2  *  k))
26.  mdist(d2;x  n;y  n)  \mleq{}  (r1/r(2  *  k))
\mvdash{}  mdist(d2;x  n;a)  \mleq{}  (r1/r(k))


By

---

Latex:
((Assert  mdist(d2;y  n;a)  \mleq{}  mdist(d1;y  n;a)  BY
                (BackThruHyp'  4  THEN  Auto))
  THEN  (Assert  mdist(d2;y  n;a)  \mleq{}  (r1/r(2  *  k))  BY
                          Auto)
  )

---

Home Index