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