---

Step * of Lemma m-open-set

No Annotations
∀[X:Type]. ∀[d:metric(X)]. ∀[A:X ⟶ ℙ].  (m-open(X;d;x.A[x]) ⇒ m-set(X;d;x.A[x]))
BY
{ (Auto
   THEN Unfold `m-open` -1
   THEN Unfold `m-set` 0
   THEN Auto
   THEN (FHyp 4 [-1] THENA Auto)
   THEN ExRepD
   THEN BHyp -1
   THEN Auto
   THEN (RWO "7" 0 THEN Auto)
   THEN RWO "mdist-same" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[A:X  {}\mrightarrow{}  \mBbbP{}].    (m-open(X;d;x.A[x])  {}\mRightarrow{}  m-set(X;d;x.A[x]))


By

---

Latex:
(Auto
  THEN  Unfold  `m-open`  -1
  THEN  Unfold  `m-set`  0
  THEN  Auto
  THEN  (FHyp  4  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  BHyp  -1
  THEN  Auto
  THEN  (RWO  "7"  0  THEN  Auto)
  THEN  RWO  "mdist-same"  0
  THEN  Auto)

---

Home Index