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. Type
2. 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