---

Step * 1 2 1 1 1 1 of Lemma injection-inverse


1. A : Type
2. B : Type
3. f : A ⟶ B@i
4. Inj(A;B;f)@i
5. a : A@i
6. n : ℕ@i
7. h : ℕn ⟶ A@i
8. Surj(ℕn;A;h)@i
9. ∀x,y:B.  Dec(x = y ∈ B)@i
10. test : b:B ⟶ (∃i:ℕn. ((f (h i)) = b ∈ B) + (¬(∃i:ℕn. ((f (h i)) = b ∈ B))))
11. a@0 : A@i
12. i : ℕn@i
13. x1 : (f (h i)) = (f a@0) ∈ B@i
14. (test (f a@0)) = (inl <i, x1>) ∈ (∃i:ℕn. ((f (h i)) = (f a@0) ∈ B) + (¬(∃i:ℕn. ((f (h i)) = (f a@0) ∈ B))))@i
⊢ (h i) = a@0 ∈ A
BY
{ Auto }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B@i
4.  Inj(A;B;f)@i
5.  a  :  A@i
6.  n  :  \mBbbN{}@i
7.  h  :  \mBbbN{}n  {}\mrightarrow{}  A@i
8.  Surj(\mBbbN{}n;A;h)@i
9.  \mforall{}x,y:B.    Dec(x  =  y)@i
10.  test  :  b:B  {}\mrightarrow{}  (\mexists{}i:\mBbbN{}n.  ((f  (h  i))  =  b)  +  (\mneg{}(\mexists{}i:\mBbbN{}n.  ((f  (h  i))  =  b))))
11.  a@0  :  A@i
12.  i  :  \mBbbN{}n@i
13.  x1  :  (f  (h  i))  =  (f  a@0)@i
14.  (test  (f  a@0))  =  (inl  <i,  x1>)@i
\mvdash{}  (h  i)  =  a@0


By

---

Latex:
Auto

---

Home Index