---

Step * 1 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|| ∈ ℤ
⊢ Surj(ℕ||as||;ℕ||as||;f)
BY
{ (BLemma `injection-is-surjection` THEN Auto) }

---

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{}  Surj(\mBbbN{}||as||;\mBbbN{}||as||;f)


By

---

Latex:
(BLemma  `injection-is-surjection`  THEN  Auto)

---

Home Index