Nuprl Definition : cantor_cauchy
cantor_cauchy(a;b;k) ==
eval x = eval y' = 0 + (b 4) in
eval y' = y' + (-(a 4)) in
y' ÷ 4 in
if (0) < (x)
then if (x + 4) ÷ 2=0 then 1 else (2 * log(2;((x + 4) ÷ 2) * k))
else if ((-x) + 4) ÷ 2=0 then 1 else (2 * log(2;(((-x) + 4) ÷ 2) * k))
Definitions occuring in Statement :
log: log(b;n),
callbyvalue: callbyvalue,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
apply: f a,
divide: n ÷ m,
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
callbyvalue: callbyvalue,
apply: f a,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
log: log(b;n),
multiply: n * m,
divide: n ÷ m,
add: n + m,
minus: -n,
natural_number: $n
FDL editor aliases :
cantor_cauchy
Latex:
cantor\_cauchy(a;b;k) ==
eval x = eval y' = 0 + (b 4) in
eval y' = y' + (-(a 4)) in
y' \mdiv{} 4 in
if (0) < (x)
then if (x + 4) \mdiv{} 2=0 then 1 else (2 * log(2;((x + 4) \mdiv{} 2) * k))
else if ((-x) + 4) \mdiv{} 2=0 then 1 else (2 * log(2;(((-x) + 4) \mdiv{} 2) * k))
Date html generated:
2019_10_30-AM-07_38_33
Last ObjectModification:
2019_02_12-AM-11_10_28
Theory : reals
Home
Index