Nuprl Definition : rat-midpoint
rat-midpoint(a;b) == rat-nat-div(ratadd(a;b);2)
Definitions occuring in Statement :
rat-nat-div: rat-nat-div(x;n),
ratadd: ratadd(x;y),
natural_number: $n
Definitions occuring in definition :
rat-nat-div: rat-nat-div(x;n),
ratadd: ratadd(x;y),
natural_number: $n
FDL editor aliases :
rat-midpoint
Latex:
rat-midpoint(a;b) == rat-nat-div(ratadd(a;b);2)
Date html generated:
2019_10_30-AM-09_31_12
Last ObjectModification:
2019_02_17-PM-06_12_37
Theory : reals
Home
Index