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

`∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:T ⟶ ℤ].`
`  (∀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` 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 :  and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` infix_ap: `x f y` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` assoc: `Assoc(T;op)` comm: `Comm(T;op)` subtype_rel: `A ⊆r B` le: `A ≤ B` empty-bag: `{}` uiff: `uiff(P;Q)` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` cons-bag: `x.b` monoid_p: `IsMonoid(T;op;id)` ident: `Ident(T;op;id)` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_uimplies: `rev_uimplies(P;Q)` sq_or: `a ↓∨ b`
Lemmas referenced :  bag_to_squash_list bag-member_wf le_wf bag-summation_wf all_wf bag_wf decidable__equal_int satisfiable-full-omega-tt 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 list_induction list-subtype-bag equal_wf list_wf bag-member-empty-iff empty-bag_wf list_accum_nil_lemma bag-member-cons cons-bag_wf itermConstant_wf int_term_value_constant_lemma squash_wf true_wf bag-summation-cons iff_weakening_equal decidable__le add-is-int-iff intformand_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_le_lemma false_wf bag-summation_functionality_wrt_le and_wf
Rules used in proof :  cut sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin isect_memberFormation introduction lambdaFormation extract_by_obid isectElimination because_Cache hypothesisEquality imageElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality cumulativity intEquality lambdaEquality addEquality natural_numberEquality sqequalRule applyEquality functionExtensionality independent_isectElimination independent_pairFormation functionEquality rename dependent_functionElimination axiomEquality isect_memberEquality equalityTransitivity universeEquality unionElimination dependent_pairFormation int_eqEquality voidElimination voidEquality computeAll independent_functionElimination independent_pairEquality imageMemberEquality baseClosed inlFormation pointwiseFunctionality baseApply closedConclusion inrFormation setElimination setEquality dependent_set_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[f,g:T  {}\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: 2017_10_01-AM-09_02_38
Last ObjectModification: 2017_07_26-PM-04_43_44

Theory : bags

Home Index