---

Step * 1 1 of Lemma inv-rel-inject

.....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?)
BY
{ xxx(AssertBY (finv (f a1)) = (inl a1) ∈ (A?) (BackThruSomeHyp THEN Auto)⋅
      THEN AssertBY (finv (f a2)) = (inl a2) ∈ (A?) (BackThruSomeHyp THEN Auto)⋅
      )xxx }

1
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. (finv (f a1)) = (inl a1) ∈ (A?)
11. (finv (f a2)) = (inl a2) ∈ (A?)
⊢ (inl a1) = (inl a2) ∈ (A?)

---

Latex:

---

Latex:
.....assertion..... 
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{}  (inl  a1)  =  (inl  a2)


By

---

Latex:
xxx(AssertBY  (finv  (f  a1))  =  (inl  a1)  (BackThruSomeHyp  THEN  Auto)\mcdot{}
        THEN  AssertBY  (finv  (f  a2))  =  (inl  a2)  (BackThruSomeHyp  THEN  Auto)\mcdot{}
        )xxx

---

Home Index