---

Step * of Lemma subtype_rel_sets_simple

∀[A:Type]. ∀[P,Q:A ⟶ ℙ].  {a:A| P[a]}  ⊆r {b:A| Q[b]}  supposing ∀a:A. (P[a] ⇒ Q[a])
BY
{ TACTIC:(Auto THEN Try (Complete ((SubsumeC ⌜{a:A| P[a]} ⌝⋅ THEN Auto)))) }

---

Latex:

---

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


By

---

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

---

Home Index