---

Step * of Lemma dist-fun_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[x:X].  (dist-fun(d;x) ∈ FUN(X ⟶ ℝ))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN Try (ProveWfLemma) THEN D 0 THEN Auto THEN RepUR ``dist-fun so_apply`` 0) }

1
1. X : Type
2. d : metric(X)
3. x : X
4. x1 : X
5. x2 : X
6. x1 ≡ x2
⊢ mdist(d;x;x1) ≡ mdist(d;x;x2)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[x:X].    (dist-fun(d;x)  \mmember{}  FUN(X  {}\mrightarrow{}  \mBbbR{}))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  (ProveWfLemma)
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``dist-fun  so\_apply``  0)

---

Home Index