Nuprl Definition : cantor-to-interval
cantor-to-interval(a;b;f) == λn.eval m = 4 * n in let x,y = cantor-interval(a;b;f;cantor_cauchy(a;b;m)) in (x m) ÷ 4
Definitions occuring in Statement :
cantor_cauchy: cantor_cauchy(a;b;k),
cantor-interval: cantor-interval(a;b;f;n),
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
spread: spread def,
divide: n ÷ m,
multiply: n * m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
callbyvalue: callbyvalue,
multiply: n * m,
spread: spread def,
cantor-interval: cantor-interval(a;b;f;n),
cantor_cauchy: cantor_cauchy(a;b;k),
divide: n ÷ m,
apply: f a,
natural_number: $n
FDL editor aliases :
cantor-to-interval
Latex:
cantor-to-interval(a;b;f) ==
\mlambda{}n.eval m = 4 * n in
let x,y = cantor-interval(a;b;f;cantor\_cauchy(a;b;m))
in (x m) \mdiv{} 4
Date html generated:
2016_05_18-AM-11_04_19
Last ObjectModification:
2015_09_23-AM-09_18_25
Theory : reals
Home
Index