---

Step * of Lemma m-interior-point_wf

No Annotations
∀[X,A:Type].  ∀[d:metric(X)]. ∀[p:A].  (m-interior-point(X;d;A;p) ∈ ℙ) supposing strong-subtype(A;X)
BY
{ (Intros
   THEN Unhide
   THEN ((RWO "strong-subtype-iff-respects-equality" 3 THENA Auto)
         THEN (InstLemma `equal-wf` [⌜X⌝;⌜X⌝;⌜A⌝]⋅ THENA Auto)
         THEN Unfold `m-interior-point` 0
         THEN GenConcl ⌜p = y ∈ X⌝⋅
         THEN Auto)⋅) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,A:Type].    \mforall{}[d:metric(X)].  \mforall{}[p:A].    (m-interior-point(X;d;A;p)  \mmember{}  \mBbbP{})  supposing  strong-subtype(A;X)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  ((RWO  "strong-subtype-iff-respects-equality"  3  THENA  Auto)
              THEN  (InstLemma  `equal-wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  Unfold  `m-interior-point`  0
              THEN  GenConcl  \mkleeneopen{}p  =  y\mkleeneclose{}\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index