### Nuprl Lemma : bag-filter-filter2

`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[q:{x:T| ↑p[x]}  ⟶ 𝔹]. ∀[bs:bag(T)].`
`  ([x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} ))`

Proof

Definitions occuring in Statement :  bag-filter: `[x∈b|p[x]]` bag: `bag(T)` band: `p ∧b q` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` bfalse: `ff` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B` sq_type: `SQType(T)` guard: `{T}` assert: `↑b` true: `True` bag-filter: `[x∈b|p[x]]` top: `Top`
Lemmas referenced :  bag_to_squash_list equal_wf bag_wf assert_wf bool_wf eqtt_to_assert bag-filter_wf subtype_rel_bag subtype_rel_sets assert_of_band assert_elim subtype_base_sq bool_subtype_base set_wf filter-filter filter_wf4_2 list-subtype-bag l_member_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis rename hyp_replacement equalitySymmetry applyLambdaEquality setEquality cumulativity applyEquality functionExtensionality because_Cache lambdaFormation unionElimination equalityElimination sqequalRule independent_isectElimination dependent_set_memberEquality equalityTransitivity dependent_functionElimination independent_functionElimination lambdaEquality setElimination addLevel levelHypothesis instantiate natural_numberEquality independent_pairFormation functionEquality universeEquality isect_memberFormation isect_memberEquality axiomEquality voidElimination voidEquality productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[q:\{x:T|  \muparrow{}p[x]\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].
([x\mmember{}[x\mmember{}bs|p[x]]|q[x]]  =  [x\mmember{}bs|p[x]  \mwedge{}\msubb{}  q[x]])

Date html generated: 2017_10_01-AM-08_45_26
Last ObjectModification: 2017_07_26-PM-04_30_42

Theory : bags

Home Index