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

[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b}  ⟶ ℤ].
  (∀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 set: {x:A| B[x]}  lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n int: universe: Type equal: 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:  Q uimplies: supposing a squash: T sq_stable: SqStable(P) assoc: Assoc(T;op) infix_ap: 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: 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

\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