### Nuprl Lemma : bag-member-mapfilter

`∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:U]. ∀[bs:bag(T)]. ∀[f:{x:T| ↑(P x)}  ⟶ U].`
`  uiff(x ↓∈ bag-mapfilter(f;P;bs);↓∃v:{x:T| ↑(P x)} . (v ↓∈ bs ∧ (x = (f v) ∈ U)))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-mapfilter: `bag-mapfilter(f;P;bs)` bag: `bag(T)` assert: `↑b` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` bag: `bag(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_apply: `x[s]` exists: `∃x:A. B[x]` uiff: `uiff(P;Q)` uimplies: `b supposing a` quotient: `x,y:A//B[x; y]` implies: `P `` Q` bag-mapfilter: `bag-mapfilter(f;P;bs)` bag-filter: `[x∈b|p[x]]` bag-map: `bag-map(f;bs)` mapfilter: `mapfilter(f;P;L)` bag-member: `x ↓∈ bs` squash: `↓T` subtype_rel: `A ⊆r B` cand: `A c∧ B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  uiff_wf bag-member_wf bag-mapfilter_wf assert_wf squash_wf exists_wf equal_wf list_wf list-subtype-bag permutation_wf equal-wf-base bag_wf bool_wf member-permutation member_wf mapfilter_wf member-mapfilter l_member_wf subtype_rel_dep_function subtype_rel_sets assert_functionality_wrt_uiff eta_conv set_wf
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalHypSubstitution pointwiseFunctionalityForEquality cut extract_by_obid isectElimination thin cumulativity hypothesisEquality because_Cache dependent_functionElimination functionExtensionality applyEquality setEquality hypothesis sqequalRule lambdaEquality lambdaFormation setElimination rename productEquality dependent_set_memberEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry independent_pairEquality isect_memberEquality imageElimination independent_isectElimination independent_functionElimination functionEquality universeEquality isect_memberFormation imageMemberEquality baseClosed dependent_pairFormation independent_pairFormation

Latex:
\mforall{}[T,U:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:U].  \mforall{}[bs:bag(T)].  \mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U].
uiff(x  \mdownarrow{}\mmember{}  bag-mapfilter(f;P;bs);\mdownarrow{}\mexists{}v:\{x:T|  \muparrow{}(P  x)\}  .  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))

Date html generated: 2017_10_01-AM-08_54_24
Last ObjectModification: 2017_07_26-PM-04_36_04

Theory : bags

Home Index