---

Step * 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 ≡(A) as'
⊢ map(f;as) ≡(B) map(f;as')
BY
{ (D 6 THEN D 0) }

1
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')|| ∈ ℤ

2
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)
8. ||map(f;as)|| = ||map(f;as')|| ∈ ℤ
⊢ ∃p:Sym(||map(f;as)||). ∀i:ℕ||map(f;as)||. (map(f;as)[p.f i] = map(f;as')[i] ∈ B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  as  :  A  List
5.  as'  :  A  List
6.  as  \mequiv{}(A)  as'
\mvdash{}  map(f;as)  \mequiv{}(B)  map(f;as')


By

---

Latex:
(D  6  THEN  D  0)

---

Home Index