---

Step * 1 1 of Lemma permutation_inversion

.....assertion..... 
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
⊢ ∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)
BY
{ Assert ⌜Surj(ℕ||as||;ℕ||as||;f)⌝⋅ }

1
.....assertion..... 
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
⊢ Surj(ℕ||as||;ℕ||as||;f)

2
1. [A] : Type
2. as : A List
3. bs : A List
4. f : ℕ||as|| ⟶ ℕ||as||
5. Inj(ℕ||as||;ℕ||as||;f)
6. bs = (as o f) ∈ (A List)
7. ||as|| = ||bs|| ∈ ℤ
8. Surj(ℕ||as||;ℕ||as||;f)
⊢ ∃g:ℕ||as|| ⟶ ℕ||as||. ∀x:ℕ||as||. ((f (g x)) = x ∈ ℤ)

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  as  :  A  List
3.  bs  :  A  List
4.  f  :  \mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||
5.  Inj(\mBbbN{}||as||;\mBbbN{}||as||;f)
6.  bs  =  (as  o  f)
7.  ||as||  =  ||bs||
\mvdash{}  \mexists{}g:\mBbbN{}||as||  {}\mrightarrow{}  \mBbbN{}||as||.  \mforall{}x:\mBbbN{}||as||.  ((f  (g  x))  =  x)


By

---

Latex:
Assert  \mkleeneopen{}Surj(\mBbbN{}||as||;\mBbbN{}||as||;f)\mkleeneclose{}\mcdot{}

---

Home Index