Nuprl Definition : ratio-dist
|a/b - p/q| < 1/m == m * |(a * q) - p * b| < b * q
Definitions occuring in Statement :
absval: |i|,
less_than: a < b,
multiply: n * m,
subtract: n - m
Definitions occuring in definition :
less_than: a < b,
absval: |i|,
subtract: n - m,
multiply: n * m
FDL editor aliases :
ratio-dist
Latex:
|a/b - p/q| < 1/m == m * |(a * q) - p * b| < b * q
Date html generated:
2016_05_15-PM-04_43_12
Last ObjectModification:
2015_09_23-AM-07_49_43
Theory : general
Home
Index