---

Step * of Lemma scale-metric-complete

∀[X:Type]. ∀[d:metric(X)].  ∀c:{c:ℝ| r0 < c} . (mcomplete(X with d) ⇐⇒ mcomplete(X with c*d))
BY
{ (InstLemma `scale-metric-cauchy` []
   THEN RepeatFor 3 (ParallelLast')
   THEN InstLemma `scale-metric-converges` [⌜X⌝;⌜d⌝;⌜c⌝]⋅
   THEN Auto
   THEN ParallelLast
   THEN All (RepUR ``mk-metric-space``)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].    \mforall{}c:\{c:\mBbbR{}|  r0  <  c\}  .  (mcomplete(X  with  d)  \mLeftarrow{}{}\mRightarrow{}  mcomplete(X  with  c*d))


By

---

Latex:
(InstLemma  `scale-metric-cauchy`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  InstLemma  `scale-metric-converges`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  All  (RepUR  ``mk-metric-space``)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index