---

Step * of Lemma null-bag-mapfilter

∀P,f,bs:Top.  (bag-null(bag-mapfilter(f;P;bs)) ~ bag-null([x∈bs|P x]))
BY
{ (Unfold `bag-null` 0 THEN InstLemma `bag-mapfilter-null` [] THEN ParallelLast) }

---

Latex:

---

Latex:
\mforall{}P,f,bs:Top.    (bag-null(bag-mapfilter(f;P;bs))  \msim{}  bag-null([x\mmember{}bs|P  x]))


By

---

Latex:
(Unfold  `bag-null`  0  THEN  InstLemma  `bag-mapfilter-null`  []  THEN  ParallelLast)

---

Home Index