Reference · Signed rationals

rainbow.math.rational.signed.limit-difference

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

The difference limit law for signed-rational sequences. `signed/subtract a b` and `signed/add a (signed/negate b)` are the *same* Grothendieck pair definitionally -- both reduce to make (positive a + negative b) (negative a + positive b) so subtraction needs no arithmetic of its own: the additive limit law applied to the negated sequence already has the subtractive type. This module records that composition as first-class theorems, closing the signed limit-arithmetic layer (sum, scalar, negation, difference). Native and axiom-free; chains the D63 limit-arithmetic and limit-negation modules.

Depends onmath.rational.signed.limit-arithmeticmath.rational.signed.limit-negate

analysis/close-subtractive :
  (L eps-left x M eps-right y : ℚ) (x-close : analysis/close L eps-left x)
  (y-close : analysis/close M eps-right y)
  → analysis/close (L - M) (eps-left + eps-right) (x - y)

analysis/limit-difference :
  (s t : ℕ → ℚ) (L M : ℚ) (Ms Mt : ℚ → ℕ) (s-converges : analysis/converges s L Ms)
  (t-converges : analysis/converges t M Mt)
  → analysis/converges (fun n => s n - t n) (L - M) (fun eps => algebra/nat-add (Ms eps) (Mt 0))