---

Step * of Lemma inject_functionality

∀[A,B,C:Type]. ∀[f:B ⟶ C].  (Inj(A;C;f)) supposing (Inj(B;C;f) and strong-subtype(A;B))
BY
{ (BasicUniformUnivCD Auto
   THEN (Unhide THENA Auto)
   THEN ((Assert A ⊆r B BY (D -2 THEN Auto)) THEN PromoteHyp (-1) (-2))⋅) }

1
1. A : Type
2. B : Type
3. C : Type
4. f : B ⟶ C
5. strong-subtype(A;B)
6. A ⊆r B
7. Inj(B;C;f)
⊢ Inj(A;C;f)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:B  {}\mrightarrow{}  C].    (Inj(A;C;f))  supposing  (Inj(B;C;f)  and  strong-subtype(A;B))


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (Unhide  THENA  Auto)
  THEN  ((Assert  A  \msubseteq{}r  B  BY  (D  -2  THEN  Auto))  THEN  PromoteHyp  (-1)  (-2))\mcdot{})

---

Home Index