### Nuprl Lemma : bag-summation_functionality_wrt_le_1

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

Proof

Definitions occuring in Statement :  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]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` int: `ℤ` universe: `Type`
Definitions unfolded in proof :  and: `P ∧ Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` so_lambda: `λ2x.t[x]` le: `A ≤ B` all: `∀x:A. B[x]` so_apply: `x[s]` cand: `A c∧ B` sq_stable: `SqStable(P)` implies: `P `` Q` exists: `∃x:A. B[x]` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` prop: `ℙ` not: `¬A` false: `False` infix_ap: `x f y` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` assoc: `Assoc(T;op)` comm: `Comm(T;op)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` less_than': `less_than'(a;b)` rev_uimplies: `rev_uimplies(P;Q)` ge: `i ≥ j ` guard: `{T}`
Lemmas referenced :  bag_to_squash_list sq_stable__le bag-summation_wf le_wf less_than'_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_accum_wf list_wf list_accum_nil_lemma list_accum_cons_lemma false_wf decidable__le intformand_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_le_lemma le_functionality add_functionality_wrt_le le_weakening
Rules used in proof :  cut sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin isect_memberFormation introduction extract_by_obid isectElimination hypothesisEquality imageElimination because_Cache sqequalRule lambdaEquality hypothesis dependent_functionElimination independent_isectElimination independent_pairFormation independent_functionElimination promote_hyp rename hyp_replacement equalitySymmetry Error :applyLambdaEquality,  cumulativity intEquality addEquality natural_numberEquality imageMemberEquality baseClosed independent_pairEquality axiomEquality equalityTransitivity applyEquality functionExtensionality isect_memberEquality functionEquality voidElimination universeEquality unionElimination dependent_pairFormation int_eqEquality voidEquality computeAll lambdaFormation

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

Date html generated: 2016_10_25-AM-10_36_00
Last ObjectModification: 2016_07_12-AM-06_50_35

Theory : bags

Home Index