Nuprl Definition : real-vec-sum
Σ{x[k] | n≤k≤m} == λi.Σ{x[k] i | n≤k≤m}
Definitions occuring in Statement :
rsum: Σ{x[k] | n≤k≤m},
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
rsum: Σ{x[k] | n≤k≤m},
apply: f a
FDL editor aliases :
real-vec-sum
Latex:
\mSigma{}\{x[k] | n\mleq{}k\mleq{}m\} == \mlambda{}i.\mSigma{}\{x[k] i | n\mleq{}k\mleq{}m\}
Date html generated:
2019_10_30-AM-08_00_12
Last ObjectModification:
2019_09_17-PM-02_22_35
Theory : reals
Home
Index