---

Step * of Lemma compact-metric-to-metric-continuity

∀X:Type. ∀d:metric(X).  (mcompact(X;d) ⇒ (∀Y:Type. ∀dY:metric(Y). ∀f:FUN(X ⟶ Y).  UC(f:X ⟶ Y)))
BY
{ (Auto
   THEN D 3
   THEN RenameVar `cmplt' 3
   THEN RenameVar `mtb' 4
   THEN (Assert ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y) BY
               (DVar `f' THEN (Unhide THENA Auto) THEN RepUR ``is-mfun`` -1 THEN Auto))
   THEN D -2
   THEN Thin (-2)
   THEN RepUR ``m-unif-cont`` 0) }

1
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
⊢ ∀k:ℕ+. ∃delta:{d:ℝ| r0 < d} . ∀x,y:X.  ((mdist(d;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k))))

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}d:metric(X).    (mcompact(X;d)  {}\mRightarrow{}  (\mforall{}Y:Type.  \mforall{}dY:metric(Y).  \mforall{}f:FUN(X  {}\mrightarrow{}  Y).    UC(f:X  {}\mrightarrow{}  Y)))


By

---

Latex:
(Auto
  THEN  D  3
  THEN  RenameVar  `cmplt'  3
  THEN  RenameVar  `mtb'  4
  THEN  (Assert  \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)  BY
                          (DVar  `f'  THEN  (Unhide  THENA  Auto)  THEN  RepUR  ``is-mfun``  -1  THEN  Auto))
  THEN  D  -2
  THEN  Thin  (-2)
  THEN  RepUR  ``m-unif-cont``  0)

---

Home Index