Nuprl Definition : atan-size-bound
atan-size-bound(x) ==  eval z = |x| 1000 in imax(2000 ÷ z + 2;2)
Definitions occuring in Statement : 
rabs: |x|, 
imax: imax(a;b), 
callbyvalue: callbyvalue, 
apply: f a, 
divide: n ÷ m, 
add: n + m, 
natural_number: $n
Definitions occuring in definition : 
callbyvalue: callbyvalue, 
apply: f a, 
rabs: |x|, 
imax: imax(a;b), 
divide: n ÷ m, 
add: n + m, 
natural_number: $n
FDL editor aliases : 
atan-size-bound
Latex:
atan-size-bound(x)  ==    eval  z  =  |x|  1000  in  imax(2000  \mdiv{}  z  +  2;2)
Date html generated:
2018_05_22-PM-03_06_33
Last ObjectModification:
2017_10_26-PM-10_33_15
Theory : reals_2
Home
Index