---

Step * of Lemma m-boundary_wf

No Annotations
∀[X,A:Type].  ∀[d:metric(X)]. (m-boundary(X;d;A) ∈ Type) supposing strong-subtype(A;X)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,A:Type].    \mforall{}[d:metric(X)].  (m-boundary(X;d;A)  \mmember{}  Type)  supposing  strong-subtype(A;X)


By

---

Latex:
ProveWfLemma

---

Home Index