Reference · Signed rationals

rainbow.math.rational.signed.limit-negate

Signed rationalssrc/rainbow/math/rational/signed/limit_negate.clj0 definitions, 2 theorems

Negation preserves signed-rational closeness and limits. D63 defines `analysis/close L eps x` as the order band L - eps <= x AND x <= L + eps. Negating reverses signed order. The two reversed endpoints reduce to the corresponding band around `-L`, so the radius and modulus are unchanged. Native and axiom-free; builds directly on the D63 convergence module.

Depends onmath.rational.signed.convergence

analysis/close-negate :
  (L eps x : ℚ) (bounded : analysis/close L eps x)
  → analysis/close (signed/negate L) eps (signed/negate x)

analysis/limit-negate :
  (s : ℕ → ℚ) (L : ℚ) (M : ℚ → ℕ) (s-converges : analysis/converges s L M)
  → analysis/converges (fun n => signed/negate (s n)) (signed/negate L) M