---

Step * of Lemma bag-combine-map

∀[A,B,C:Type]. ∀[g:B ⟶ bag(C)]. ∀[f:A ⟶ B]. ∀[bs:bag(A)].  (⋃x∈bag-map(f;bs).g[x] = ⋃x∈bs.g[f x] ∈ bag(C))
BY
{ (Auto
   THEN BagD (-1)
   THEN Auto
   THEN (Subst' as = bs ∈ bag(A) 0 THENA Auto)
   THEN ThinVar `as'
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto) }

1
1. A : Type
2. B : Type
3. C : Type
4. g : B ⟶ bag(C)
5. f : A ⟶ B
6. u : A
7. v : A List
8. ⋃x∈bag-map(f;v).g[x] = ⋃x∈v.g[f x] ∈ bag(C)
⊢ ⋃x∈bag-map(f;[u / v]).g[x] = ⋃x∈[u / v].g[f x] ∈ bag(C)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[bs:bag(A)].    (\mcup{}x\mmember{}bag-map(f;bs).g[x]  =  \mcup{}x\mmember{}bs.g[f  x])


By

---

Latex:
(Auto
  THEN  BagD  (-1)
  THEN  Auto
  THEN  (Subst'  as  =  bs  0  THENA  Auto)
  THEN  ThinVar  `as'
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index