---

Step * of Lemma bag-mapfilter-null

∀P,f,bs:Top.  (null(bag-mapfilter(f;P;bs)) ~ null([x∈bs|P x]))
BY
{ (Unfold `bag-mapfilter` 0 THEN (UnivCD THENA Auto) THEN RWO "bag-map-null" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `bag-mapfilter`  0  THEN  (UnivCD  THENA  Auto)  THEN  RWO  "bag-map-null"  0  THEN  Auto)

---

Home Index