Nuprl Lemma : vs_bag_add_empty_lemma
∀f,vs:Top. (Σ{f | b ∈ {}} ~ 0)
Proof
Definitions occuring in Statement :
vs-bag-add: Σ{f[b] | b ∈ bs},
vs-0: 0,
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t,
empty-bag: {}
Definitions unfolded in proof :
all: ∀x:A. B[x],
vs-bag-add: Σ{f[b] | b ∈ bs},
bag-summation: Σ(x∈b). f[x],
bag-accum: bag-accum(v,x.f[v; x];init;bs),
list_accum: list_accum,
empty-bag: {},
nil: [],
it: ⋅,
vs-0: 0,
record-select: r.x,
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}f,vs:Top. (\mSigma{}\{f | b \mmember{} \{\}\} \msim{} 0)
Date html generated:
2019_10_31-AM-06_25_50
Last ObjectModification:
2019_08_07-PM-03_18_38
Theory : linear!algebra
Home
Index