Nuprl Definition : cantor_to_interval
cantor_to_interval(a;b;f) == a + ((b - a/r1 + (b - a)) * (cantor-to-interval(a;b + r1;f) - a))
Definitions occuring in Statement :
cantor-to-interval: cantor-to-interval(a;b;f),
rdiv: (x/y),
rsub: x - y,
rmul: a * b,
radd: a + b,
int-to-real: r(n),
natural_number: $n
Definitions occuring in definition :
rmul: a * b,
rdiv: (x/y),
rsub: x - y,
cantor-to-interval: cantor-to-interval(a;b;f),
radd: a + b,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
cantor_to_interval
Latex:
cantor\_to\_interval(a;b;f) == a + ((b - a/r1 + (b - a)) * (cantor-to-interval(a;b + r1;f) - a))
Date html generated:
2018_05_22-PM-02_10_12
Last ObjectModification:
2017_10_06-AM-11_08_39
Theory : reals
Home
Index