### Nuprl Lemma : sub-bag-filter

`∀[T:Type]. ∀p:T ⟶ 𝔹. ∀b,c:bag(T).  (sub-bag(T;b;[x∈c|p[x]]) `⇐⇒` sub-bag(T;b;c) ∧ (∀x:T. (x ↓∈ b `` (↑p[x]))))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` sub-bag: `sub-bag(T;as;bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` cand: `A c∧ B` member: `t ∈ T` so_apply: `x[s]` prop: `ℙ` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` rev_implies: `P `` Q` uimplies: `b supposing a` uiff: `uiff(P;Q)` sub-bag: `sub-bag(T;as;bs)` exists: `∃x:A. B[x]` top: `Top` respects-equality: `respects-equality(S;T)` true: `True` squash: `↓T` guard: `{T}`
Lemmas referenced :  assert_witness bag-member_wf sub-bag_wf bag-filter_wf istype-assert bag_wf bool_wf istype-universe bag-split sub-bag-append-trivial1 bnot_wf sub-bag-member bag-member-filter equal_wf subtype_rel_bag assert_wf bag-filter-append istype-void bag-append_wf respects-equality-bag subtype-respects-equality bag-filter-trivial2 iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt independent_pairFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality independent_functionElimination universeIsType because_Cache sqequalRule lambdaEquality_alt productElimination productIsType functionIsType inhabitedIsType instantiate universeEquality dependent_functionElimination hyp_replacement equalitySymmetry applyLambdaEquality independent_isectElimination equalityTransitivity setEquality setElimination rename setIsType isect_memberEquality_alt voidElimination dependent_pairFormation_alt equalityIstype productEquality natural_numberEquality imageElimination imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type]
\mforall{}p:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}b,c:bag(T).
(sub-bag(T;b;[x\mmember{}c|p[x]])  \mLeftarrow{}{}\mRightarrow{}  sub-bag(T;b;c)  \mwedge{}  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p[x]))))

Date html generated: 2019_10_15-AM-11_02_00
Last ObjectModification: 2018_11_30-AM-10_08_19

Theory : bags

Home Index