---

Step * 2 of Lemma metric-subspace_wf


1. X : Type
2. d : metric(X)
3. A : Type
4. strong-subtype(A;X)
⊢ ∀a:A. ∀x:X.  (x ≡ a ⇒ (x ∈ A)) ∈ Type
BY
{ ((RWO "strong-subtype-iff-respects-equality" (-1) THENA Auto)
   THEN (InstLemma `equal-wf` [⌜X⌝;⌜X⌝;⌜A⌝]⋅ THENA Auto)
   THEN (MemCD THENL [Auto; (GenConcl ⌜a = y ∈ X⌝⋅ THEN Auto)])) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  A  :  Type
4.  strong-subtype(A;X)
\mvdash{}  \mforall{}a:A.  \mforall{}x:X.    (x  \mequiv{}  a  {}\mRightarrow{}  (x  \mmember{}  A))  \mmember{}  Type


By

---

Latex:
((RWO  "strong-subtype-iff-respects-equality"  (-1)  THENA  Auto)
  THEN  (InstLemma  `equal-wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (MemCD  THENL  [Auto;  (GenConcl  \mkleeneopen{}a  =  y\mkleeneclose{}\mcdot{}  THEN  Auto)]))

---

Home Index