Nuprl Lemma : trivial-null-formal-sum
∀K:Rng. ∀[S:Type]. ∀fs:basic-formal-sum(K;S). null-formal-sum(K;S;fs + -(fs))
Proof
Definitions occuring in Statement :
null-formal-sum: null-formal-sum(K;S;fs),
neg-bfs: -(fs),
basic-formal-sum: basic-formal-sum(K;S),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
universe: Type,
rng: Rng,
bag-append: as + bs
Definitions unfolded in proof :
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
subtype_rel: A ⊆r B,
rng: Rng,
top: Top,
zero-bfs: 0 * ss,
basic-formal-sum: basic-formal-sum(K;S),
member: t ∈ T,
exists: ∃x:A. B[x],
null-formal-sum: null-formal-sum(K;S;fs),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Lemmas referenced :
rng_wf,
basic-formal-sum_wf,
exists_wf,
zero-bfs_wf,
bag_wf,
equal_wf,
bag-append_wf,
rng_car_wf,
bag-subtype-list,
neg-bfs_wf,
bag-append-empty,
bag-append-assoc,
bag_map_empty_lemma,
empty-bag_wf
Rules used in proof :
universeEquality,
lambdaEquality,
because_Cache,
productEquality,
applyEquality,
rename,
setElimination,
voidEquality,
voidElimination,
isect_memberEquality,
dependent_functionElimination,
sqequalRule,
hypothesis,
cumulativity,
thin,
isectElimination,
extract_by_obid,
introduction,
cut,
hypothesisEquality,
sqequalHypSubstitution,
dependent_pairFormation,
isect_memberFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}K:Rng. \mforall{}[S:Type]. \mforall{}fs:basic-formal-sum(K;S). null-formal-sum(K;S;fs + -(fs))
Date html generated:
2018_05_22-PM-09_47_20
Last ObjectModification:
2018_01_08-PM-02_28_52
Theory : linear!algebra
Home
Index