---

Step * of Lemma m-strong-extensionality

∀[X:Type]. ∀d:metric(X). (mcomplete(X with d) ⇒ (∀Y:Type. ∀d':metric(Y). ∀f:FUN(X ⟶ Y).  is-msfun(X;d;Y;d';f)))
BY
{ (InstLemma `metric-strong-extensionality` []
   THEN RepeatFor 3 (ParallelLast')
   THEN Auto
   THEN D -1
   THEN Unhide
   THEN Auto
   THEN InstHyp [⌜Y⌝;⌜d'⌝;⌜f⌝] 4⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X)
        (mcomplete(X  with  d)  {}\mRightarrow{}  (\mforall{}Y:Type.  \mforall{}d':metric(Y).  \mforall{}f:FUN(X  {}\mrightarrow{}  Y).    is-msfun(X;d;Y;d';f)))


By

---

Latex:
(InstLemma  `metric-strong-extensionality`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  Auto
  THEN  D  -1
  THEN  Unhide
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  4\mcdot{}
  THEN  Auto)

---

Home Index