---

Step * of Lemma bag-map-union

∀[T,S:Type]. ∀[f:T ⟶ bag(S)]. ∀[bbs:bag(bag(T))].
  (bag-map(f;bag-union(bbs)) = bag-union(bag-map(λb.bag-map(f;b);bbs)) ∈ bag(bag(S)))
BY
{ (Auto THEN BagD (-1) THEN Auto) }

1
1. T : Type
2. S : Type
3. f : T ⟶ bag(S)
4. as : bag(T) List
5. bs : bag(T) List
6. permutation(bag(T);as;bs)
⊢ bag-map(f;bag-union(as)) = bag-union(bag-map(λb.bag-map(f;b);bs)) ∈ bag(bag(S))

---

Latex:

---

Latex:
\mforall{}[T,S:Type].  \mforall{}[f:T  {}\mrightarrow{}  bag(S)].  \mforall{}[bbs:bag(bag(T))].
    (bag-map(f;bag-union(bbs))  =  bag-union(bag-map(\mlambda{}b.bag-map(f;b);bbs)))


By

---

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

---

Home Index