---

Step * 1 1 of Lemma inject-composes


1. A : Type
2. B0 : Type
3. B1 : Type
4. C : Type
5. f : A ⟶ B0
6. g : B1 ⟶ C
7. strong-subtype(B0;B1)
8. Inj(A;B0;f)
9. Inj(B1;C;g)
10. ∀b:B1. ∀a:B0.  ((b = a ∈ B1) ⇒ (b = a ∈ B0))
⊢ Inj(A;C;g o f)
BY
{ Assert ⌜∀x:A. (f x ∈ B1)⌝⋅ }

1
.....assertion..... 
1. A : Type
2. B0 : Type
3. B1 : Type
4. C : Type
5. f : A ⟶ B0
6. g : B1 ⟶ C
7. strong-subtype(B0;B1)
8. Inj(A;B0;f)
9. Inj(B1;C;g)
10. ∀b:B1. ∀a:B0.  ((b = a ∈ B1) ⇒ (b = a ∈ B0))
⊢ ∀x:A. (f x ∈ B1)

2
1. A : Type
2. B0 : Type
3. B1 : Type
4. C : Type
5. f : A ⟶ B0
6. g : B1 ⟶ C
7. strong-subtype(B0;B1)
8. Inj(A;B0;f)
9. Inj(B1;C;g)
10. ∀b:B1. ∀a:B0.  ((b = a ∈ B1) ⇒ (b = a ∈ B0))
11. ∀x:A. (f x ∈ B1)
⊢ Inj(A;C;g o f)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B0  :  Type
3.  B1  :  Type
4.  C  :  Type
5.  f  :  A  {}\mrightarrow{}  B0
6.  g  :  B1  {}\mrightarrow{}  C
7.  strong-subtype(B0;B1)
8.  Inj(A;B0;f)
9.  Inj(B1;C;g)
10.  \mforall{}b:B1.  \mforall{}a:B0.    ((b  =  a)  {}\mRightarrow{}  (b  =  a))
\mvdash{}  Inj(A;C;g  o  f)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x:A.  (f  x  \mmember{}  B1)\mkleeneclose{}\mcdot{}

---

Home Index