Nuprl Lemma : mset_count_union

s:DSet. ∀as,bs:MSet{s}. ∀c:|s|.  ((c #∈ (as ⋃ bs)) imax(c #∈ as;c #∈ bs) ∈ ℤ)


Proof




Definitions occuring in Statement :  mset_union: a ⋃ b mset_count: #∈ a mset: MSet{s} imax: imax(a;b) all: x:A. B[x] int: equal: t ∈ T dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] dset: DSet mset: MSet{s} quotient: x,y:A//B[x; y] and: P ∧ Q implies:  Q mset_count: #∈ a mset_union: a ⋃ b prop: squash: T true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  set_car_wf mset_wf dset_wf list_wf permr_wf equal_wf equal-wf-base squash_wf true_wf count_functionality lmax_wf lmax_functionality_wrt_permr imax_wf count_wf iff_weakening_equal count_lmax
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality dependent_functionElimination pointwiseFunctionalityForEquality intEquality sqequalRule pertypeElimination productElimination equalityTransitivity equalitySymmetry because_Cache independent_functionElimination productEquality applyEquality lambdaEquality imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed independent_isectElimination

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:MSet\{s\}.  \mforall{}c:|s|.    ((c  \#\mmember{}  (as  \mcup{}  bs))  =  imax(c  \#\mmember{}  as;c  \#\mmember{}  bs))



Date html generated: 2017_10_01-AM-09_59_53
Last ObjectModification: 2017_03_03-PM-01_00_48

Theory : mset


Home Index