### Nuprl Lemma : bag-member-map

`∀[T,U:Type].  ∀x:U. ∀f:T ⟶ U. ∀bs:bag(T).  uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-map: `bag-map(f;bs)` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` bag-member: `x ↓∈ bs` so_lambda: `λ2x.t[x]` so_apply: `x[s]` exists: `∃x:A. B[x]` implies: `P `` Q` subtype_rel: `A ⊆r B` bag-map: `bag-map(f;bs)` top: `Top` empty-bag: `{}` false: `False` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` single-bag: `{x}` bag-append: `as + bs` iff: `P `⇐⇒` Q` sq_or: `a ↓∨ b` or: `P ∨ Q` rev_implies: `P `` Q` cand: `A c∧ B` cons-bag: `x.b` rev_uimplies: `rev_uimplies(P;Q)` guard: `{T}` sq_stable: `SqStable(P)`
Lemmas referenced :  bag-member_wf bag-map_wf squash_wf exists_wf equal_wf bag_wf bag_to_squash_list list_induction list-subtype-bag list_wf map_nil_lemma empty-bag_wf bag-member-empty-iff list_ind_cons_lemma list_ind_nil_lemma bag-map-append single-bag_wf top_wf bag-member-append map_cons_lemma cons_wf bag-member-single bag-member-cons sq_stable__bag-member map_wf member_map l_member_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation independent_pairFormation sqequalHypSubstitution imageElimination hypothesis sqequalRule imageMemberEquality hypothesisEquality thin baseClosed extract_by_obid isectElimination cumulativity functionExtensionality applyEquality lambdaEquality productEquality functionEquality dependent_functionElimination productElimination independent_pairEquality isect_memberEquality equalityTransitivity equalitySymmetry because_Cache universeEquality hyp_replacement applyLambdaEquality independent_functionElimination independent_isectElimination rename voidElimination voidEquality unionElimination dependent_pairFormation inlFormation inrFormation

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

Date html generated: 2017_10_01-AM-08_54_08
Last ObjectModification: 2017_07_26-PM-04_35_53

Theory : bags

Home Index