---

Step * of Lemma strong-subtype-set1

∀[A:Type]. ∀[P,Q:A ⟶ ℙ].  strong-subtype({x:A| P[x]} ;{x:A| Q[x]} ) supposing ∀x:A. (P[x] ⇒ Q[x])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P,Q:A  {}\mrightarrow{}  \mBbbP{}].    strong-subtype(\{x:A|  P[x]\}  ;\{x:A|  Q[x]\}  )  supposing  \mforall{}x:A.  (P[x]  {}\mRightarrow{}  Q[x])


By

---

Latex:
Auto

---

Home Index