Nuprl Definition : series-sum
Note that in Σn.x[n] = a, the index n is in ℕ  (i.e, 0,1,2,...) rather
than ℕ+  (1,2,3,...) as in Bishop & Bridges.⋅
Σn.x[n] = a ==  lim n→∞.Σ{x[i] | 0≤i≤n} = a
Definitions occuring in Statement : 
rsum: Σ{x[k] | n≤k≤m}
, 
converges-to: lim n→∞.x[n] = y
, 
natural_number: $n
Definitions occuring in definition : 
converges-to: lim n→∞.x[n] = y
, 
rsum: Σ{x[k] | n≤k≤m}
, 
natural_number: $n
FDL editor aliases : 
series-sum
series-sum
Latex:
\mSigma{}n.x[n]  =  a  ==    lim  n\mrightarrow{}\minfty{}.\mSigma{}\{x[i]  |  0\mleq{}i\mleq{}n\}  =  a
Date html generated:
2016_11_08-AM-09_00_32
Last ObjectModification:
2016_11_05-AM-11_36_44
Theory : reals
Home
Index