---

Step * of Lemma set-metric-subspace

∀[X:Type]. ∀[d:metric(X)]. ∀[P:X ⟶ ℙ].  metric-subspace(X;d;{x:X| P[x]} ) supposing ∀x,y:X.  (P[x] ⇒ y ≡ x ⇒ P[y])
BY
{ (Auto THEN (D 0 THENL [Auto; ((D 0 THENA Auto) THEN D -1 THEN Auto)])) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[P:X  {}\mrightarrow{}  \mBbbP{}].    metric-subspace(X;d;\{x:X|  P[x]\}  )  supposing  \mforall{}x,y:X.    (P[x]  \000C{}\mRightarrow{}  y  \mequiv{}  x  {}\mRightarrow{}  P[y])


By

---

Latex:
(Auto  THEN  (D  0  THENL  [Auto;  ((D  0  THENA  Auto)  THEN  D  -1  THEN  Auto)]))

---

Home Index