Nuprl Definition : small-real-test
small-real-test(k;z) ==  rless-case((r1)/k;(r(4))/k;k;z)
Definitions occuring in Statement : 
rless-case: rless-case(x;y;n;z)
, 
int-rdiv: (a)/k1
, 
int-to-real: r(n)
, 
natural_number: $n
Definitions occuring in definition : 
int-rdiv: (a)/k1
, 
int-to-real: r(n)
, 
natural_number: $n
FDL editor aliases : 
small-real-test
Latex:
small-real-test(k;z)  ==    rless-case((r1)/k;(r(4))/k;k;z)
Date html generated:
2019_10_29-AM-10_04_48
Last ObjectModification:
2019_06_19-PM-05_05_25
Theory : reals
Home
Index