---

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

.....antecedent..... 
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. c2*d2 ≤ d1
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)
⊢ d2 ≤ (r1/c1 * c2)*c1*d1
BY
{ (RepeatFor 2 (ParallelOp -7)
   THEN ParallelLast
   THEN (Unhide THENA Auto)
   THEN MoveToConcl (-1)
   THEN RepUR ``mdist scale-metric`` 0
   THEN Fold `mdist` 0
   THEN GenConclTerms Auto [⌜mdist(d2;x1;y)⌝;⌜mdist(d1;x1;y)⌝]⋅) }

1
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))

---

Latex:

---

Latex:
.....antecedent..... 
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.  c2*d2  \mleq{}  d1
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)
\mvdash{}  d2  \mleq{}  (r1/c1  *  c2)*c1*d1


By

---

Latex:
(RepeatFor  2  (ParallelOp  -7)
  THEN  ParallelLast
  THEN  (Unhide  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``mdist  scale-metric``  0
  THEN  Fold  `mdist`  0
  THEN  GenConclTerms  Auto  [\mkleeneopen{}mdist(d2;x1;y)\mkleeneclose{};\mkleeneopen{}mdist(d1;x1;y)\mkleeneclose{}]\mcdot{})

---

Home Index