---

Step * of Lemma set-metric-subspace2

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

---

Latex:

---

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


By

---

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

---

Home Index