---

Step * of Lemma subtype_rel_sets

∀[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:A| P[a]\000C}  ⊆r B))
BY
{ (Auto THEN Try (Complete ((SubsumeC ⌜{a:A| P[a]} ⌝⋅ THEN Auto)))) }

1
1. A : Type
2. B : Type
3. P : A ⟶ ℙ
4. Q : B ⟶ ℙ
5. {a:A| P[a]}  ⊆r B
6. ∀a:A. (P[a] ⇒ Q[a])
⊢ {a:A| P[a]}  ⊆r {b:B| Q[b]} 

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Try  (Complete  ((SubsumeC  \mkleeneopen{}\{a:A|  P[a]\}  \mkleeneclose{}\mcdot{}  THEN  Auto))))

---

Home Index