### Nuprl Lemma : sub-bag-mapfilter-implies

`∀[A,B:Type].`
`  ∀as:bag(A). ∀bs:bag(B). ∀f:A ⟶ B. ∀P:A ⟶ 𝔹.  (sub-bag(B;bag-map(f;as);bs) `` sub-bag(B;bag-mapfilter(f;P;as);bs))`

Proof

Definitions occuring in Statement :  sub-bag: `sub-bag(T;as;bs)` bag-mapfilter: `bag-mapfilter(f;P;bs)` bag-map: `bag-map(f;bs)` bag: `bag(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` sub-bag: `sub-bag(T;as;bs)` bag-mapfilter: `bag-mapfilter(f;P;bs)` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top`
Lemmas referenced :  bag-filter-split equal_wf bag_wf bag-append_wf bag-map_wf bag-map-append bag-filter_wf subtype_rel_bag top_wf assert_wf bnot_wf subtype_rel_dep_function set_wf bag-append-assoc sub-bag_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid isectElimination hypothesisEquality equalitySymmetry hypothesis hyp_replacement Error :applyLambdaEquality,  cumulativity equalityTransitivity functionExtensionality applyEquality sqequalRule lambdaEquality setEquality independent_isectElimination isect_memberEquality voidElimination voidEquality because_Cache dependent_pairFormation setElimination rename functionEquality

Latex:
\mforall{}[A,B:Type].
\mforall{}as:bag(A).  \mforall{}bs:bag(B).  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.
(sub-bag(B;bag-map(f;as);bs)  {}\mRightarrow{}  sub-bag(B;bag-mapfilter(f;P;as);bs))

Date html generated: 2016_10_25-AM-10_38_00
Last ObjectModification: 2016_07_12-AM-06_51_32

Theory : bags

Home Index