Nuprl Lemma : r-list-sum_wf
∀[L:ℝ List]. (r-list-sum(L) ∈ ℝ)
Proof
Definitions occuring in Statement :
r-list-sum: r-list-sum(L),
real: ℝ,
list: T List,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
r-list-sum: r-list-sum(L)
Lemmas referenced :
radd_wf,
real_wf,
reduce_wf,
int-to-real_wf,
list_wf
Rules used in proof :
cut,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality_alt,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
inhabitedIsType,
universeIsType,
isect_memberFormation_alt,
sqequalRule,
natural_numberEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[L:\mBbbR{} List]. (r-list-sum(L) \mmember{} \mBbbR{})
Date html generated:
2019_10_29-AM-10_20_08
Last ObjectModification:
2019_09_18-PM-05_02_27
Theory : reals
Home
Index