Nuprl Lemma : rng_lsum_nil_lemma
∀f,r:Top. (Σ{r} x ∈ []. f[x] ~ 0)
Proof
Definitions occuring in Statement :
rng_lsum: Σ{r} x ∈ as. f[x],
nil: [],
top: Top,
so_apply: x[s],
all: ∀x:A. B[x],
sqequal: s ~ t,
rng_zero: 0
Definitions unfolded in proof :
top: Top,
member: t ∈ T,
all: ∀x:A. B[x],
rng_lsum: Σ{r} x ∈ as. f[x]
Lemmas referenced :
top_wf,
reduce_nil_lemma,
map_nil_lemma
Rules used in proof :
lambdaFormation,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}f,r:Top. (\mSigma{}\{r\} x \mmember{} []. f[x] \msim{} 0)
Date html generated:
2018_05_21-PM-09_32_40
Last ObjectModification:
2017_12_11-PM-00_49_14
Theory : matrices
Home
Index