Reference · Signed rationals

rainbow.math.rational.signed.order-respects

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

Equivalence transport for signed order and signed-sequence convergence. The order proof uses two copies of the reorder-and-cancel argument from signed/at-most-transitive. First it transports the left endpoint through a signed equivalence, then it transports the right endpoint. In each pass an equivalence is viewed as an nnrat inequality, added to the current order proof, reordered so a common right summand is visible, and cancelled. The convergence theorem is the first limit law unlocked by that transport: replacing every term of a convergent signed sequence by an equivalent term preserves the same limit and modulus. Native and axiom-free; chains signed convergence (and hence signed-order-transitivity plus its D63 nnrat toolkit).

Depends onmath.rational.signed.convergence

signed/at-most-respects-equivalence :
  (a ah b bh : ℚ)
  (a-eq : a = ah)
  (b-eq : b = bh)
  (ordered : a ≤ b)
  → ah ≤ bh

analysis/converges-respects-pointwise-equivalence :
  (s t : ℕ → ℚ) (L : ℚ) (M : ℚ → ℕ)
  (pointwise : ∀ (n : ℕ), s n = t n)
  (s-converges : analysis/converges s L M)
  → analysis/converges t L M