Nuprl Definition : cantor_ivl
cantor_ivl(a;b;f;n) ==
let k,j = unit-interval-fan(f;n)
in eval d = 3^n in
<eval k' = d - k in (k' * a + k * b)/d, eval j' = d - j in (j' * a + j * b)/d>
Definitions occuring in Statement :
unit-interval-fan: unit-interval-fan(f;n),
int-rdiv: (a)/k1,
int-rmul: k1 * a,
radd: a + b,
callbyvalue: callbyvalue,
spread: spread def,
pair: <a, b>,
subtract: n - m,
natural_number: $n,
fastexp: i^n
Definitions occuring in definition :
spread: spread def,
unit-interval-fan: unit-interval-fan(f;n),
fastexp: i^n,
natural_number: $n,
pair: <a, b>,
callbyvalue: callbyvalue,
subtract: n - m,
int-rdiv: (a)/k1,
radd: a + b,
int-rmul: k1 * a
FDL editor aliases :
cantor_ivl
Latex:
cantor\_ivl(a;b;f;n) ==
let k,j = unit-interval-fan(f;n)
in eval d = 3\^{}n in
<eval k' = d - k in (k' * a + k * b)/d, eval j' = d - j in (j' * a + j * b)/d>
Date html generated:
2016_05_18-AM-10_55_12
Last ObjectModification:
2015_09_23-AM-09_17_59
Theory : reals
Home
Index