---

Step * of Lemma bag-mapfilter_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index