Nuprl Definition : real-from-approx
real-from-approx(n.x[n]) == cauchy-limit(n.x[n + 1];λk.(2 * k))
Definitions occuring in Statement :
cauchy-limit: cauchy-limit(n.x[n];c),
lambda: λx.A[x],
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
cauchy-limit: cauchy-limit(n.x[n];c),
add: n + m,
lambda: λx.A[x],
multiply: n * m,
natural_number: $n
FDL editor aliases :
real-from-approx
Latex:
real-from-approx(n.x[n]) == cauchy-limit(n.x[n + 1];\mlambda{}k.(2 * k))
Date html generated:
2018_05_22-PM-01_50_56
Last ObjectModification:
2017_10_24-PM-11_46_22
Theory : reals
Home
Index