### Nuprl Lemma : bag-member-product

`∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[p:A × B].  uiff(p ↓∈ as × bs;fst(p) ↓∈ as ∧ snd(p) ↓∈ bs)`

Proof

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

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[p:A  \mtimes{}  B].    uiff(p  \mdownarrow{}\mmember{}  as  \mtimes{}  bs;fst(p)  \mdownarrow{}\mmember{}  as  \mwedge{}  snd(p)  \mdownarrow{}\mmember{}  bs)

Date html generated: 2017_10_01-AM-08_54_39
Last ObjectModification: 2017_07_26-PM-04_36_25

Theory : bags

Home Index