Nuprl Definition : real-ratio-bound
real-ratio-bound(M;x;y;a;b) ==
eval c = rclose-or-sep(M;x;y) in
if (c =z 1) then (a/y - x)
if (c =z 2) then (b/x - y)
else (r(M)/r(2)) * rmin(a;b)
fi
Definitions occuring in Statement :
rclose-or-sep: rclose-or-sep(K;x;y),
rdiv: (x/y),
rmin: rmin(x;y),
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n
FDL editor aliases :
real-ratio-bound
Latex:
real-ratio-bound(M;x;y;a;b) ==
eval c = rclose-or-sep(M;x;y) in
if (c =\msubz{} 1) then (a/y - x)
if (c =\msubz{} 2) then (b/x - y)
else (r(M)/r(2)) * rmin(a;b)
fi
Date html generated:
2020_05_20-AM-11_06_49
Last ObjectModification:
2019_11_06-PM-05_49_43
Theory : reals
Home
Index