Nuprl Definition : rat-int-bound

rat-int-bound(q) ==  let n,r = rat-int-part(q) in if qeq(r;0) then n else n + 1 fi 


Definitions occuring in Statement :  rat-int-part: rat-int-part(q),  qeq: qeq(r;s),  ifthenelse: if b then t else f fi ,  spread: spread def,  add: n + m,  natural_number: $n
Definitions occuring in definition :  spread: spread def,  rat-int-part: rat-int-part(q),  ifthenelse: if b then t else f fi ,  qeq: qeq(r;s),  add: n + m,  natural_number: $n
FDL editor aliases :  rat-int-bound
Latex:
rat-int-bound(q)  ==    let  n,r  =  rat-int-part(q)  in  if  qeq(r;0)  then  n  else  n  +  1  fi 


Date html generated: 2016_05_15-PM-11_34_20
Last ObjectModification: 2015_09_23-AM-08_30_12

Theory : rationals


Home Index