---

Step * of Lemma sq_exists_subtype_rel

∀[A,B:Type]. ∀[P:A ⟶ ℙ]. ∀[Q:B ⟶ ℙ].
  ((∃a:{A| P[a]}) ⊆r (∃b:{B| Q[b]})) supposing ((∀a:A. (P[a] ⇒ Q[a])) and (A ⊆r B))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:B  {}\mrightarrow{}  \mBbbP{}].
    ((\mexists{}a:\{A|  P[a]\})  \msubseteq{}r  (\mexists{}b:\{B|  Q[b]\}))  supposing  ((\mforall{}a:A.  (P[a]  {}\mRightarrow{}  Q[a]))  and  (A  \msubseteq{}r  B))


By

---

Latex:
Auto

---

Home Index