Nuprl Lemma : real-rng_lsum-sq
∀[L,A:Top]. (Σ{real-ring()} x ∈ L. A[x] ~ reduce(λx,y. (x + y);r0;map(λx.A[x];L)))
Proof
Definitions occuring in Statement :
real-ring: real-ring(),
radd: a + b,
int-to-real: r(n),
map: map(f;as),
reduce: reduce(f;k;as),
uall: ∀[x:A]. B[x],
top: Top,
so_apply: x[s],
lambda: λx.A[x],
natural_number: $n,
sqequal: s ~ t,
rng_lsum: Σ{r} x ∈ as. f[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rng_lsum: Σ{r} x ∈ as. f[x],
real-ring: real-ring(),
rng_plus: +r,
pi2: snd(t),
pi1: fst(t),
rng_zero: 0
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
hypothesis,
axiomSqEquality,
inhabitedIsType,
hypothesisEquality,
sqequalHypSubstitution,
isect_memberEquality_alt,
isectElimination,
thin,
isectIsTypeImplies,
extract_by_obid
Latex:
\mforall{}[L,A:Top]. (\mSigma{}\{real-ring()\} x \mmember{} L. A[x] \msim{} reduce(\mlambda{}x,y. (x + y);r0;map(\mlambda{}x.A[x];L)))
Date html generated:
2019_10_30-AM-08_10_13
Last ObjectModification:
2019_09_18-PM-04_26_41
Theory : reals
Home
Index