Nuprl Lemma : bag-filter-empty

[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  ∀x:T. (x ↓∈  (¬↑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: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] not: ¬A implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  not: ¬A implies:  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 ⊆B uimplies: supposing a true: True bag-filter: [x∈b|p[x]] bag-null: bag-null(bs) uiff: uiff(P;Q) iff: ⇐⇒ Q rev_implies:  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