### Nuprl Lemma : bag-filter-empty

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  ∀x:T. (x ↓∈ b `` (¬↑P[x])) supposing ↑bag-null([x∈b|P[x]])`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-null: `bag-null(bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  not: `¬A` implies: `P `` Q` bag-member: `x ↓∈ bs` squash: `↓T` false: `False` exists: `∃x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` prop: `ℙ` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` true: `True` bag-filter: `[x∈b|p[x]]` bag-null: `bag-null(bs)` uiff: `uiff(P;Q)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` guard: `{T}`
Lemmas referenced :  true_wf squash_wf assert_functionality_wrt_uiff bool_wf bag_wf bag-member_wf nil_member sqequal-nil member-filter l_member_wf filter_wf5 assert_of_null list-subtype-bag bag-filter_wf assert_wf bag-null_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution imageElimination cut productElimination thin hypothesis because_Cache lemma_by_obid dependent_functionElimination setEquality hypothesisEquality isectElimination applyEquality sqequalRule lambdaEquality independent_isectElimination natural_numberEquality setElimination rename dependent_set_memberEquality independent_functionElimination equalityTransitivity equalitySymmetry voidElimination functionEquality universeEquality isect_memberFormation introduction isect_memberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:bag(T)].    \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\mneg{}\muparrow{}P[x]))  supposing  \muparrow{}bag-null([x\mmember{}b|P[x]])

Date html generated: 2016_05_15-PM-02_44_28
Last ObjectModification: 2016_01_16-AM-08_45_08

Theory : bags

Home Index