---

Step * 1 of Lemma injection-inverse


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)
BY
{ Assert ⌜∀b:B. Dec(∃i:ℕn. ((f (h i)) = b ∈ B))⌝⋅ }

1
.....assertion..... 
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
⊢ ∀b:B. Dec(∃i:ℕn. ((f (h i)) = b ∈ B))

2
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
9. ∀b:B. Dec(∃i:ℕn. ((f (h i)) = b ∈ B))
⊢ ∃g:B ⟶ A. ∀a:A. ((g (f a)) = a ∈ A)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  f  :  A  \mrightarrow{}{}\mrightarrow{}  B@i
4.  a  :  A@i
5.  n  :  \mBbbN{}@i
6.  h  :  \mBbbN{}n  {}\mrightarrow{}  A@i
7.  Surj(\mBbbN{}n;A;h)@i
8.  \mforall{}x,y:B.    Dec(x  =  y)@i
\mvdash{}  \mexists{}g:B  {}\mrightarrow{}  A.  \mforall{}a:A.  ((g  (f  a))  =  a)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}b:B.  Dec(\mexists{}i:\mBbbN{}n.  ((f  (h  i))  =  b))\mkleeneclose{}\mcdot{}

---

Home Index