---

Step * 1 1 of Lemma bag-map-no-repeats


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ T2
4. bs : T1 List
5. Inj(T1;T2;f)
6. L : T2 List
7. L = map(f;bs) ∈ pertype(λas,bs. ((as ∈ T2 List) ∧ (bs ∈ T2 List) ∧ permutation(T2;as;bs)))
8. L ∈ T2 List
9. map(f;bs) ∈ T2 List
10. permutation(T2;L;map(f;bs))
11. no_repeats(T2;L)
12. bs = bs ∈ bag(T1)
13. i : ℕ
14. j : ℕ
15. i < ||bs||
16. j < ||bs||
17. ¬(i = j ∈ ℕ)
18. bs[i] = bs[j] ∈ T1
⊢ map(f;bs)[i] = map(f;bs)[j] ∈ T2
BY
{ (RWO "select-map" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  T2
4.  bs  :  T1  List
5.  Inj(T1;T2;f)
6.  L  :  T2  List
7.  L  =  map(f;bs)
8.  L  \mmember{}  T2  List
9.  map(f;bs)  \mmember{}  T2  List
10.  permutation(T2;L;map(f;bs))
11.  no\_repeats(T2;L)
12.  bs  =  bs
13.  i  :  \mBbbN{}
14.  j  :  \mBbbN{}
15.  i  <  ||bs||
16.  j  <  ||bs||
17.  \mneg{}(i  =  j)
18.  bs[i]  =  bs[j]
\mvdash{}  map(f;bs)[i]  =  map(f;bs)[j]


By

---

Latex:
(RWO  "select-map"  0  THEN  Auto)

---

Home Index