---

Step * 1 1 of Lemma map_permr_func


1. A : Type
2. B : Type
3. f : A ⟶ B
4. as : A List
5. as' : A List
6. ||as|| = ||as'|| ∈ ℤ
7. ∃p:Sym(||as||). ∀i:ℕ||as||. (as[p.f i] = as'[i] ∈ A)
⊢ ||map(f;as)|| = ||map(f;as')|| ∈ ℤ
BY
{ Auto' }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  as  :  A  List
5.  as'  :  A  List
6.  ||as||  =  ||as'||
7.  \mexists{}p:Sym(||as||).  \mforall{}i:\mBbbN{}||as||.  (as[p.f  i]  =  as'[i])
\mvdash{}  ||map(f;as)||  =  ||map(f;as')||


By

---

Latex:
Auto'

---

Home Index