---

Step * of Lemma bag-mapfilter-fast-eq2

∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].
  (bag-mapfilter(f;P;bs) = bag-mapfilter-fast(f;P;bs) ∈ bag(B))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B].
    (bag-mapfilter(f;P;bs)  =  bag-mapfilter-fast(f;P;bs))


By

---

Latex:
Auto

---

Home Index