---

Step * of Lemma bag-filter-is-nil

∀[T:Type]. ∀[p:T ⟶ 𝔹].  ∀[bs:bag(T)]. ([x∈bs|p[x]] ~ []) supposing ∀x:T. (¬↑p[x])
BY
{ Auto }

1
1. T : Type
2. p : T ⟶ 𝔹
3. ∀x:T. (¬↑p[x])
4. bs : bag(T)
⊢ [x∈bs|p[x]] ~ []

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index