---

Step * of Lemma names-hom-subtype

∀[I1,J1,I2,J2:fset(ℕ)].  (I1 ⟶ J1 ⊆r I2 ⟶ J2) supposing (J2 ⊆ J1 and I1 ⊆ I2)
BY
{ (Auto THEN Unfold `names-hom` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I1,J1,I2,J2:fset(\mBbbN{})].    (I1  {}\mrightarrow{}  J1  \msubseteq{}r  I2  {}\mrightarrow{}  J2)  supposing  (J2  \msubseteq{}  J1  and  I1  \msubseteq{}  I2)


By

---

Latex:
(Auto  THEN  Unfold  `names-hom`  0  THEN  Auto)

---

Home Index