Nuprl Definition : cantor-interval
cantor-interval(a;b;f;n) ==
primrec(n;<a, b>;λi,p. let a',b' = p in if f i then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/3> fi )
Definitions occuring in Statement :
int-rdiv: (a)/k1,
int-rmul: k1 * a,
radd: a + b,
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
spread: spread def,
ifthenelse: if b then t else f fi ,
apply: f a,
pair: <a, b>,
int-rdiv: (a)/k1,
radd: a + b,
int-rmul: k1 * a,
natural_number: $n
FDL editor aliases :
cantor-interval
Latex:
cantor-interval(a;b;f;n) ==
primrec(n;<a, b>\mlambda{}i,p. let a',b' = p in if f i then <(2 * a' + b')/3, b'> else <a', (a' + 2 * b')/\000C3> fi )
Date html generated:
2016_05_18-AM-10_55_47
Last ObjectModification:
2015_09_23-AM-09_18_07
Theory : reals
Home
Index