Reference · Signed rationals

rainbow.math.rational.signed.limit-order

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

Limits preserve the pointwise order of signed-rational sequences. The convergence predicate ranges over every signed radius, including zero. At the common index Ms(0)+Mt(0), zero-radius convergence gives L <= s(n) and t(n) <= M after transporting the endpoints through the established signed-zero equivalences. The pointwise hypothesis and signed order transitivity then give L <= s(n) <= t(n) <= M. Native and axiom-free; chains the D63 convergence/order toolkit through signed limit uniqueness (which supplies signed/add-zero-right).

Depends onmath.rational.signed.limit-uniqueness

analysis/limit-preserves-order :
  (s t : ℕ → ℚ) (L M : ℚ) (Ms Mt : ℚ → ℕ)
  (pointwise : ∀ (n : ℕ), s n ≤ t n)
  (s-converges : analysis/converges s L Ms) (t-converges : analysis/converges t M Mt)
  → L ≤ M