Nuprl Lemma : bag-summation-single
∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].
∀[T:Type]. ∀[f:T ⟶ R]. ∀[a:T]. (Σ(x∈{a}). f[x] = f[a] ∈ R) supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
Proof
Definitions occuring in Statement :
bag-summation: Σ(x∈b). f[x],
single-bag: {x},
comm: Comm(T;op),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
so_apply: x[s],
and: P ∧ Q,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T,
monoid_p: IsMonoid(T;op;id)
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
and: P ∧ Q,
monoid_p: IsMonoid(T;op;id),
assoc: Assoc(T;op),
ident: Ident(T;op;id),
infix_ap: x f y,
prop: ℙ
Lemmas referenced :
bag-summation-single-sq,
istype-void,
monoid_p_wf,
comm_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalTransitivity,
computationStep,
isectElimination,
thin,
isect_memberEquality_alt,
voidElimination,
hypothesis,
isect_memberFormation_alt,
productElimination,
applyEquality,
hypothesisEquality,
universeIsType,
axiomEquality,
isectIsTypeImplies,
inhabitedIsType,
functionIsType,
productIsType,
because_Cache,
instantiate,
universeEquality
Latex:
\mforall{}[R:Type]. \mforall{}[add:R {}\mrightarrow{} R {}\mrightarrow{} R]. \mforall{}[zero:R].
\mforall{}[T:Type]. \mforall{}[f:T {}\mrightarrow{} R]. \mforall{}[a:T]. (\mSigma{}(x\mmember{}\{a\}). f[x] = f[a])
supposing IsMonoid(R;add;zero) \mwedge{} Comm(R;add)
Date html generated:
2019_10_15-AM-11_00_42
Last ObjectModification:
2019_08_13-PM-00_01_48
Theory : bags
Home
Index