---

Step * of Lemma induced-metric_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[Y:Type]. ∀[f:Y ⟶ X].  (induced-metric(d;f) ∈ metric(Y))
BY
{ (Auto
   THEN DVar `d'
   THEN (Assert induced-metric(d;f) ∈ Y ⟶ Y ⟶ ℝ BY
               ProveWfLemma)
   THEN MemTypeCD
   THEN Auto
   THEN All (RepUR ``induced-metric``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[Y:Type].  \mforall{}[f:Y  {}\mrightarrow{}  X].    (induced-metric(d;f)  \mmember{}  metric(Y))


By

---

Latex:
(Auto
  THEN  DVar  `d'
  THEN  (Assert  induced-metric(d;f)  \mmember{}  Y  {}\mrightarrow{}  Y  {}\mrightarrow{}  \mBbbR{}  BY
                          ProveWfLemma)
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  (RepUR  ``induced-metric``)
  THEN  Auto)

---

Home Index