---

Step * of Lemma compact-dist_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[A:Type].  ∀[c:mcompact(A;d)]. ∀[x:X].  (dist(x;A) ∈ ℝ) supposing A ⊆r X
BY
{ (Auto THEN (Assert dist-fun(d;x) ∈ FUN(A ⟶ ℝ) BY (DoSubsume THEN Auto)) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[A:Type].
    \mforall{}[c:mcompact(A;d)].  \mforall{}[x:X].    (dist(x;A)  \mmember{}  \mBbbR{})  supposing  A  \msubseteq{}r  X


By

---

Latex:
(Auto  THEN  (Assert  dist-fun(d;x)  \mmember{}  FUN(A  {}\mrightarrow{}  \mBbbR{})  BY  (DoSubsume  THEN  Auto))  THEN  ProveWfLemma)

---

Home Index