---

Step * 1 1 1 of Lemma equiv-metrics-preserve-complete


1. X : Type
2. d1 : metric(X)
3. d2 : metric(X)
4. c1 : {s:ℝ| r0 < s} 
5. c2 : {s:ℝ| r0 < s} 
6. ∀x,y:X.  (mdist(c1*d1;x;y) ≤ mdist(d2;x;y))
7. c2*d2 ≤ d1
8. mcomplete(X with d1)
9. r0 < (c1 * c2)
10. r0 < (r1/c1 * c2)
11. x : ℕ ⟶ X
12. mcauchy(c2*d2;n.x n)
13. subsequence(a,b.a ≡ b;n.x n;n.x n)
14. x1 : X
15. ∀y:X. (mdist(c1*d1;x1;y) ≤ mdist(d2;x1;y))
16. y : X
17. v : ℝ
18. mdist(d2;x1;y) = v ∈ ℝ
19. v1 : ℝ
20. mdist(d1;x1;y) = v1 ∈ ℝ
⊢ ((c1 * v1) ≤ v) ⇒ (v1 ≤ ((r1/c1 * c2) * c2 * v))
BY
{ ((D 0 THENA Auto) THEN nRMul ⌜c1⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d1  :  metric(X)
3.  d2  :  metric(X)
4.  c1  :  \{s:\mBbbR{}|  r0  <  s\} 
5.  c2  :  \{s:\mBbbR{}|  r0  <  s\} 
6.  \mforall{}x,y:X.    (mdist(c1*d1;x;y)  \mleq{}  mdist(d2;x;y))
7.  c2*d2  \mleq{}  d1
8.  mcomplete(X  with  d1)
9.  r0  <  (c1  *  c2)
10.  r0  <  (r1/c1  *  c2)
11.  x  :  \mBbbN{}  {}\mrightarrow{}  X
12.  mcauchy(c2*d2;n.x  n)
13.  subsequence(a,b.a  \mequiv{}  b;n.x  n;n.x  n)
14.  x1  :  X
15.  \mforall{}y:X.  (mdist(c1*d1;x1;y)  \mleq{}  mdist(d2;x1;y))
16.  y  :  X
17.  v  :  \mBbbR{}
18.  mdist(d2;x1;y)  =  v
19.  v1  :  \mBbbR{}
20.  mdist(d1;x1;y)  =  v1
\mvdash{}  ((c1  *  v1)  \mleq{}  v)  {}\mRightarrow{}  (v1  \mleq{}  ((r1/c1  *  c2)  *  c2  *  v))


By

---

Latex:
((D  0  THENA  Auto)  THEN  nRMul  \mkleeneopen{}c1\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index