---

Step * 1 2 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||)
8. ∀i:ℕ||as||. (as[p.f i] = as'[i] ∈ A)
9. ||map(f;as)|| = ||map(f;as')|| ∈ ℤ
10. i : ℕ||map(f;as)||
⊢ map(f;as)[p.f i] = map(f;as')[i] ∈ B
BY
{ (RewriteWith [8] ``map_select`` 0 THEN 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.  p  :  Sym(||as||)
8.  \mforall{}i:\mBbbN{}||as||.  (as[p.f  i]  =  as'[i])
9.  ||map(f;as)||  =  ||map(f;as')||
10.  i  :  \mBbbN{}||map(f;as)||
\mvdash{}  map(f;as)[p.f  i]  =  map(f;as')[i]


By

---

Latex:
(RewriteWith  [8]  ``map\_select``  0  THEN  Auto')

---

Home Index