Reference · Signed rationals

rainbow.math.rational.signed.close-of-distance

Signed rationalssrc/rainbow/math/rational/signed/close_of_distance.clj0 definitions, 1 theorems

B6f lever: build a closeness band from a distance bound (the converse of dist-of-close). analysis/close-of-distance-at-most : distance x L <= eps -> close L eps x close L eps x = (L - eps <= x) AND (x <= L + eps). From |x-L| <= eps: x - L <= |x-L| <= eps (at-most-absolute) -> x <= L + eps L - x ~ -(x-L) <= |x-L| <= eps (negate-at-most-absolute + negate-subtract) -> L - eps <= x assembled with proposition/conjoin. The limit-reciprocal assembly proves distance (reciprocal (s n)) (reciprocal L) <= eps and lands the goal close (reciprocal L) eps (reciprocal (s n)) via this bridge. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.absolutemath.rational.signed.distancemath.rational.signed.additive-distancemath.rational.signed.convergencemath.rational.signed.order-transitivitymath.rational.signed.order-respects

analysis/close-of-distance-at-most :
  (L eps x : ℚ)
  (hd : signed/distance x L ≤ eps)
  → analysis/close L eps x