Reference · Signed rationals

rainbow.math.rational.signed.close-radius-monotone

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

Band weakening: a closeness band only widens with its radius. analysis/close-radius-monotone : close L r x -> r <= r' -> close L r' x. From close = (L-r<=x) AND (x<=L+r): L-r'<=L-r<=x (negate-reverses-order + add-monotone) and x<=L+r<=L+r' (add-monotone). Axiom-free; additive. A generally useful analysis lemma (and the >=-relaxation the limit-product assembly wants).

Depends onmath.rational.signed.convergencemath.rational.signed.absolute-signmath.rational.signed.distance-triangle

analysis/close-radius-monotone :
  (L r x r2 : ℚ) (hc : analysis/close L r x)
  (hr : r ≤ r2)
  → analysis/close L r2 x