---

Step * 2 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. c1*d1 ≤ d2
7. ∀x,y:X.  (mdist(c2*d2;x;y) ≤ mdist(d1;x;y))
8. mcomplete(X with d2)
9. r0 < (c1 * c2)
10. r0 < (r1/c1 * c2)
11. x : ℕ ⟶ X
12. mcauchy(c1*d1;n.x n)
13. subsequence(a,b.a ≡ b;n.x n;n.x n)
14. x1 : X
15. ∀y:X. (mdist(c2*d2;x1;y) ≤ mdist(d1;x1;y))
16. y : X
17. v : ℝ
18. mdist(d2;x1;y) = v ∈ ℝ
19. v1 : ℝ
20. mdist(d1;x1;y) = v1 ∈ ℝ
⊢ ((c2 * v) ≤ v1) ⇒ (v ≤ ((r1/c1 * c2) * c1 * v1))
BY
{ ((D 0 THENA Auto) THEN nRMul ⌜c2⌝ 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.  c1*d1  \mleq{}  d2
7.  \mforall{}x,y:X.    (mdist(c2*d2;x;y)  \mleq{}  mdist(d1;x;y))
8.  mcomplete(X  with  d2)
9.  r0  <  (c1  *  c2)
10.  r0  <  (r1/c1  *  c2)
11.  x  :  \mBbbN{}  {}\mrightarrow{}  X
12.  mcauchy(c1*d1;n.x  n)
13.  subsequence(a,b.a  \mequiv{}  b;n.x  n;n.x  n)
14.  x1  :  X
15.  \mforall{}y:X.  (mdist(c2*d2;x1;y)  \mleq{}  mdist(d1;x1;y))
16.  y  :  X
17.  v  :  \mBbbR{}
18.  mdist(d2;x1;y)  =  v
19.  v1  :  \mBbbR{}
20.  mdist(d1;x1;y)  =  v1
\mvdash{}  ((c2  *  v)  \mleq{}  v1)  {}\mRightarrow{}  (v  \mleq{}  ((r1/c1  *  c2)  *  c1  *  v1))


By

---

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

---

Home Index