---

Step * of Lemma bag-filter-wf3

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  ([x∈bs|p[x]] ∈ bag(T))
BY
{ (InstLemma `bag-filter_wf` [] THEN RepeatFor 3 (ParallelLast) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    ([x\mmember{}bs|p[x]]  \mmember{}  bag(T))


By

---

Latex:
(InstLemma  `bag-filter\_wf`  []  THEN  RepeatFor  3  (ParallelLast)  THEN  Auto)

---

Home Index