### Nuprl Lemma : mset_mem_mon_for_union

`∀s,s':DSet. ∀a:MSet{s}. ∀e:|s| ⟶ MSet{s'}. ∀x:|s'|.  x ∈b msFor{<MSet{s'},⋃,0>} y ∈ a. e[y] = ∃b{s} y ∈ a. (x ∈b e[y])`

Proof

Definitions occuring in Statement :  mset_union_mon: `<MSet{s},⋃,0>` mset_for: mset_for mset_mem: mset_mem mset: `MSet{s}` bool: `𝔹` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` equal: `s = t ∈ T` bor_mon: `<𝔹,∨b>` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` dset: `DSet` subtype_rel: `A ⊆r B` monoid_hom: `MonHom(M1,M2)` mset_union_mon: `<MSet{s},⋃,0>` grp_car: `|g|` pi1: `fst(t)` bor_mon: `<𝔹,∨b>` abmonoid: `AbMon` mon: `Mon` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  set_car_wf mset_wf dset_wf dist_hom_over_mset_for mset_union_mon_wf abmonoid_subtype_iabmonoid bor_mon_wf mset_union_bor_mon_hom mset_mem_wf bool_wf grp_car_wf abmonoid_wf monoid_hom_p_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality functionEquality dependent_functionElimination sqequalRule applyEquality dependent_set_memberEquality lambdaEquality because_Cache

Latex:
\mforall{}s,s':DSet.  \mforall{}a:MSet\{s\}.  \mforall{}e:|s|  {}\mrightarrow{}  MSet\{s'\}.  \mforall{}x:|s'|.
x  \mmember{}\msubb{}  msFor\{<MSet\{s'\},\mcup{},0>\}  y  \mmember{}  a.  e[y]  =  \mexists{}\msubb{}\{s\}  y  \mmember{}  a.  (x  \mmember{}\msubb{}  e[y])

Date html generated: 2016_05_16-AM-07_49_57
Last ObjectModification: 2015_12_28-PM-06_01_25

Theory : mset

Home Index