### Nuprl Lemma : bag-summation-equal-implies-all-equal

`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b}  ⟶ ℤ].`
`  (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b `` (f[x] ≤ g[x]))))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` prop: `ℙ` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` implies: `P `` Q` uimplies: `b supposing a` squash: `↓T` sq_stable: `SqStable(P)` assoc: `Assoc(T;op)` infix_ap: `x f y` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` comm: `Comm(T;op)` so_lambda: `λ2x.t[x]` guard: `{T}` and: `P ∧ Q` cand: `A c∧ B`
Lemmas referenced :  bag_wf bag-subtype bag-member_wf bag-summation-equal-implies-all-equal-1 le_wf decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermAdd_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf bag-summation_wf bag-member-subtype-2 sq_stable__bag-member
Rules used in proof :  universeEquality intEquality universeIsType setIsType functionIsType inhabitedIsType equalitySymmetry equalityTransitivity dependent_functionElimination cumulativity hypothesis hypothesisEquality setEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution because_Cache dependent_set_memberEquality applyEquality sqequalRule lemma_by_obid lambdaFormation independent_isectElimination imageElimination baseClosed imageMemberEquality independent_functionElimination rename setElimination unionElimination natural_numberEquality approximateComputation dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality axiomEquality addEquality functionExtensionality independent_pairFormation

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[f,g:\{x:T|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbZ{}].
(\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  =  g[x])))  supposing
((\mSigma{}(x\mmember{}b).  g[x]  \mleq{}  \mSigma{}(x\mmember{}b).  f[x])  and
(\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  \mleq{}  g[x]))))

Date html generated: 2019_10_15-AM-11_03_56
Last ObjectModification: 2018_09_27-AM-11_07_29

Theory : bags

Home Index