---

Step * of Lemma bag-filter-is-sub-bag

∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b:bag(T).  sub-bag(T;[x∈b|p[x]];b)
BY
{ (InstLemma `bag-filter-split` [] THEN RepeatFor 3 (ParallelLast') THEN With ⌜[x∈b|¬bp[x]]⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `bag-filter-split`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  With  \mkleeneopen{}[x\mmember{}b|\mneg{}\msubb{}p[x]]\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index