---

Step * of Lemma equiv-metrics-preserve-complete

∀[X:Type]. ∀[d1,d2:metric(X)].
  ((∃c1,c2:{s:ℝ| r0 < s} . (c1*d1 ≤ d2 ∧ c2*d2 ≤ d1)) ⇒ (mcomplete(X with d1) ⇐⇒ mcomplete(X with d2)))
BY
{ (Auto
   THEN ExRepD
   THEN (Assert r0 < (c1 * c2) BY
               (DSetVars THEN Unhide THEN EAuto 1))
   THEN (Assert r0 < (r1/c1 * c2) BY
               (nRMul ⌜c1 * c2⌝ 0⋅ THEN Auto))) }

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. c2*d2 ≤ d1
8. mcomplete(X with d1)
9. r0 < (c1 * c2)
10. r0 < (r1/c1 * c2)
⊢ mcomplete(X with d2)

2
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)
⊢ mcomplete(X with d1)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d1,d2:metric(X)].
    ((\mexists{}c1,c2:\{s:\mBbbR{}|  r0  <  s\}  .  (c1*d1  \mleq{}  d2  \mwedge{}  c2*d2  \mleq{}  d1))
    {}\mRightarrow{}  (mcomplete(X  with  d1)  \mLeftarrow{}{}\mRightarrow{}  mcomplete(X  with  d2)))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (Assert  r0  <  (c1  *  c2)  BY
                          (DSetVars  THEN  Unhide  THEN  EAuto  1))
  THEN  (Assert  r0  <  (r1/c1  *  c2)  BY
                          (nRMul  \mkleeneopen{}c1  *  c2\mkleeneclose{}  0\mcdot{}  THEN  Auto)))

---

Home Index