---

Step * of Lemma isect_subtype

∀[A1:Type]. ∀[B1:A1 ⟶ ℙ]. ∀[A2:Type]. ∀[B2:A2 ⟶ ℙ].
  ((⋂x:A1. B1[x]) ⊆r (⋂x:A2. B2[x])) supposing ((∀x:A2. (B1[x] ⊆r B2[x])) and (A2 ⊆r A1))
BY
{ (Auto THEN Try ((DoSubsume THEN Auto)) THEN All (Unfold `so_apply`) THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A1:Type].  \mforall{}[B1:A1  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[A2:Type].  \mforall{}[B2:A2  {}\mrightarrow{}  \mBbbP{}].
    ((\mcap{}x:A1.  B1[x])  \msubseteq{}r  (\mcap{}x:A2.  B2[x]))  supposing  ((\mforall{}x:A2.  (B1[x]  \msubseteq{}r  B2[x]))  and  (A2  \msubseteq{}r  A1))


By

---

Latex:
(Auto  THEN  Try  ((DoSubsume  THEN  Auto))  THEN  All  (Unfold  `so\_apply`)  THEN  D  0  THEN  Auto)

---

Home Index