---

Step * of Lemma bag-map-filter

∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
  ∀[L:bag(T)]. (bag-map(f;[x∈L|P[x]]) = [x∈bag-map(f;L)|Q[x]] ∈ bag(A)) supposing ∀x:T. Q[f x] = P[x]
BY
{ ((Auto THEN BagD (-1)) THENA Auto) }

1
1. T : Type
2. A : Type
3. f : T ⟶ A
4. P : T ⟶ 𝔹
5. Q : A ⟶ 𝔹
6. ∀x:T. Q[f x] = P[x]
7. as : T List
8. bs : T List
9. permutation(T;as;bs)
⊢ bag-map(f;[x∈as|P[x]]) = [x∈bag-map(f;bs)|Q[x]] ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[Q:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[L:bag(T)].  (bag-map(f;[x\mmember{}L|P[x]])  =  [x\mmember{}bag-map(f;L)|Q[x]])  supposing  \mforall{}x:T.  Q[f  x]  =  P[x]


By

---

Latex:
((Auto  THEN  BagD  (-1))  THENA  Auto)

---

Home Index