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

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


Definitions occuring in Statement :  bag-member: x ↓∈ bs bag-summation: Σ(x∈b). f[x] bag: bag(T) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B all: x:A. B[x] implies:  Q lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  and: P ∧ Q uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] implies:  Q squash: T exists: x:A. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B infix_ap: 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 ⊆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: λ2y.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: ⇐⇒ 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

\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