---

Step * 1 of Lemma inv-rel-inject


1. A : Type
2. B : Type
3. f : A ⟶ B
4. finv : B ⟶ (A?)
5. ∀a:A. ∀b:B.  (((finv b) = (inl a) ∈ (A?)) ⇒ (b = (f a) ∈ B))
6. ∀a:A. ((finv (f a)) = (inl a) ∈ (A?))
7. a1 : A
8. a2 : A
9. (f a1) = (f a2) ∈ B
⊢ a1 = a2 ∈ A
BY
{ Assert (inl a1) = (inl a2) ∈ (A?)⋅ }

1
.....assertion..... 
1. A : Type
2. B : Type
3. f : A ⟶ B
4. finv : B ⟶ (A?)
5. ∀a:A. ∀b:B.  (((finv b) = (inl a) ∈ (A?)) ⇒ (b = (f a) ∈ B))
6. ∀a:A. ((finv (f a)) = (inl a) ∈ (A?))
7. a1 : A
8. a2 : A
9. (f a1) = (f a2) ∈ B
⊢ (inl a1) = (inl a2) ∈ (A?)

2
1. A : Type
2. B : Type
3. f : A ⟶ B
4. finv : B ⟶ (A?)
5. ∀a:A. ∀b:B.  (((finv b) = (inl a) ∈ (A?)) ⇒ (b = (f a) ∈ B))
6. ∀a:A. ((finv (f a)) = (inl a) ∈ (A?))
7. a1 : A
8. a2 : A
9. (f a1) = (f a2) ∈ B
10. (inl a1) = (inl a2) ∈ (A?)
⊢ a1 = a2 ∈ A

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  finv  :  B  {}\mrightarrow{}  (A?)
5.  \mforall{}a:A.  \mforall{}b:B.    (((finv  b)  =  (inl  a))  {}\mRightarrow{}  (b  =  (f  a)))
6.  \mforall{}a:A.  ((finv  (f  a))  =  (inl  a))
7.  a1  :  A
8.  a2  :  A
9.  (f  a1)  =  (f  a2)
\mvdash{}  a1  =  a2


By

---

Latex:
Assert  (inl  a1)  =  (inl  a2)\mcdot{}

---

Home Index