---

Step * of Lemma bag-filter-map

∀[f,p,as:Top].  ([x∈bag-map(f;as)|p[x]] ~ bag-map(f;[x∈as|p[f x]]))
BY
{ (Auto THEN Unfolds ``bag-filter bag-map`` 0 THEN RWO "filter-map" 0 THEN Auto) }

1
1. f : Top
2. p : Top
3. as : Top
⊢ (λx.p[x]) o f ~ λx.p[f x]

---

Latex:

---

Latex:
\mforall{}[f,p,as:Top].    ([x\mmember{}bag-map(f;as)|p[x]]  \msim{}  bag-map(f;[x\mmember{}as|p[f  x]]))


By

---

Latex:
(Auto  THEN  Unfolds  ``bag-filter  bag-map``  0  THEN  RWO  "filter-map"  0  THEN  Auto)

---

Home Index