Step
*
1
2
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
9. ∀b:B. Dec(∃i:ℕn. ((f (h i)) = b ∈ B))
⊢ ∃g:B ⟶ A. ∀a:A. ((g (f a)) = a ∈ A)
BY
{ (RenameVar `test' (-1) THEN RepUR ``all decidable or`` -1) }
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
9. test : b:B ⟶ (∃i:ℕn. ((f (h i)) = b ∈ B) + (¬(∃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
9. \mforall{}b:B. Dec(\mexists{}i:\mBbbN{}n. ((f (h i)) = b))
\mvdash{} \mexists{}g:B {}\mrightarrow{} A. \mforall{}a:A. ((g (f a)) = a)
By
Latex:
(RenameVar `test' (-1) THEN RepUR ``all decidable or`` -1)
Home
Index