Nuprl Lemma : rng_lsum_cons_lemma
∀f,v,u,r:Top. (Σ{r} x ∈ [u / v]. f[x] ~ f[u] +r Σ{r} x ∈ v. f[x])
Proof
Definitions occuring in Statement :
rng_lsum: Σ{r} x ∈ as. f[x],
cons: [a / b],
top: Top,
infix_ap: x f y,
so_apply: x[s],
all: ∀x:A. B[x],
sqequal: s ~ t,
rng_plus: +r
Definitions unfolded in proof :
top: Top,
member: t ∈ T,
all: ∀x:A. B[x],
infix_ap: x f y,
rng_lsum: Σ{r} x ∈ as. f[x]
Lemmas referenced :
top_wf,
reduce_cons_lemma,
map_cons_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,v,u,r:Top. (\mSigma{}\{r\} x \mmember{} [u / v]. f[x] \msim{} f[u] +r \mSigma{}\{r\} x \mmember{} v. f[x])
Date html generated:
2018_05_21-PM-09_32_41
Last ObjectModification:
2017_12_11-PM-00_41_38
Theory : matrices
Home
Index