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