---

Step * of Lemma injection-inverse

∀[A,B:Type].  ∀f:A →⟶ B. (A ⇒ finite-type(A) ⇒ (∀x,y:B.  Dec(x = y ∈ B)) ⇒ (∃g:B ⟶ A. ∀a:A. ((g (f a)) = a ∈ A)))
BY
{ (Auto THEN RenameVar `a' (-3) THEN D -2 THEN ExRepD THEN RenameVar `h' (-3)) }

1
1. [A] : Type
2. [B] : Type
3. f : A →⟶ B@i
4. a : A@i
5. n : ℕ@i
6. h : ℕn ⟶ A@i
7. Surj(ℕn;A;h)@i
8. ∀x,y:B.  Dec(x = y ∈ B)@i
⊢ ∃g:B ⟶ A. ∀a:A. ((g (f a)) = a ∈ A)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}f:A  \mrightarrow{}{}\mrightarrow{}  B.  (A  {}\mRightarrow{}  finite-type(A)  {}\mRightarrow{}  (\mforall{}x,y:B.    Dec(x  =  y))  {}\mRightarrow{}  (\mexists{}g:B  {}\mrightarrow{}  A.  \mforall{}a:A.  ((g  (f  a))  =  a)))


By

---

Latex:
(Auto  THEN  RenameVar  `a'  (-3)  THEN  D  -2  THEN  ExRepD  THEN  RenameVar  `h'  (-3))

---

Home Index