---

Step * of Lemma bag-mapfilter-combine

∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[P:B ⟶ 𝔹]. ∀[g:{x:B| ↑P[x]}  ⟶ C].
  (bag-mapfilter(g;P;⋃x∈b.f[x]) = ⋃x∈b.bag-mapfilter(g;P;f[x]) ∈ bag(C))
BY
{ (Auto
   THEN RepUR ``bag-mapfilter`` 0
   THEN (RWO "bag-filter-combine2" 0 THENA Auto)
   THEN (RWO "bag-map-combine" 0 THENA Auto)) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[b:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[g:\{x:B|  \muparrow{}P[x]\}    {}\mrightarrow{}  C].
    (bag-mapfilter(g;P;\mcup{}x\mmember{}b.f[x])  =  \mcup{}x\mmember{}b.bag-mapfilter(g;P;f[x]))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-mapfilter``  0
  THEN  (RWO  "bag-filter-combine2"  0  THENA  Auto)
  THEN  (RWO  "bag-map-combine"  0  THENA  Auto))

---

Home Index