---

Step * 2 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. c2*d2 ≤ d1
8. mcomplete(X with d2)
9. r0 < (c1 * c2)
10. r0 < (r1/c1 * c2)
⊢ mcomplete(X with d1)
BY
{ ((InstLemma `metric-leq-complete` [⌜X⌝;⌜d2⌝;⌜c1*d1⌝]⋅ THENA Auto)
   THENL [((D 0 With ⌜x⌝  THEN Auto)
           THENL [(D 0 With ⌜0⌝  THEN Auto)
                 ; (InstLemma `metric-leq-cauchy` [⌜X⌝;⌜d2⌝;⌜c1*d1⌝;⌜(r1/c1 * c2)⌝]⋅ THEN Auto)]
         )
         ; (InstLemma `scale-metric-complete` [⌜X⌝;⌜d1⌝]⋅ THEN Auto)]
) }

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

---

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.  c2*d2  \mleq{}  d1
8.  mcomplete(X  with  d2)
9.  r0  <  (c1  *  c2)
10.  r0  <  (r1/c1  *  c2)
\mvdash{}  mcomplete(X  with  d1)


By

---

Latex:
((InstLemma  `metric-leq-complete`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{};\mkleeneopen{}c1*d1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THENL  [((D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)
                  THENL  [(D  0  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)
                              ;  (InstLemma  `metric-leq-cauchy`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d2\mkleeneclose{};\mkleeneopen{}c1*d1\mkleeneclose{};\mkleeneopen{}(r1/c1  *  c2)\mkleeneclose{}]\mcdot{}  THEN  Auto)]
              )
              ;  (InstLemma  `scale-metric-complete`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d1\mkleeneclose{}]\mcdot{}  THEN  Auto)]
)

---

Home Index