### Nuprl Lemma : bag-mapfilter_wf

`∀[T,A:Type].  ∀P:T ⟶ 𝔹. ∀f:{x:T| ↑(P x)}  ⟶ A. ∀bs:bag(T).  (bag-mapfilter(f;P;bs) ∈ bag(A))`

Proof

Definitions occuring in Statement :  bag-mapfilter: `bag-mapfilter(f;P;bs)` bag: `bag(T)` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` bag-mapfilter: `bag-mapfilter(f;P;bs)` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  bag-map_wf assert_wf bag-filter_wf bag_wf bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setEquality applyEquality hypothesis lambdaEquality functionEquality dependent_functionElimination axiomEquality equalityTransitivity equalitySymmetry because_Cache universeEquality isect_memberEquality

Latex:
\mforall{}[T,A:Type].    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  A.  \mforall{}bs:bag(T).    (bag-mapfilter(f;P;bs)  \mmember{}  bag(A))

Date html generated: 2016_05_15-PM-02_23_46
Last ObjectModification: 2015_12_27-AM-09_53_56

Theory : bags

Home Index