---

Step * of Lemma mtb-cantor-map_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[cmplt:mcomplete(X with d)]. ∀[mtb:m-TB(X;d)]. ∀[p:mtb-cantor(mtb)].
  (mtb-cantor-map(d;cmplt;mtb;p) ∈ X)
BY
{ (Intros THEN (InstLemma `m-regularize-mcauchy` [⌜X⌝;⌜d⌝]⋅ THENA Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[cmplt:mcomplete(X  with  d)].  \mforall{}[mtb:m-TB(X;d)].  \mforall{}[p:mtb-cantor(mtb)].
    (mtb-cantor-map(d;cmplt;mtb;p)  \mmember{}  X)


By

---

Latex:
(Intros  THEN  (InstLemma  `m-regularize-mcauchy`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index