Reference · Signed rationals

rainbow.math.rational.signed.limit-uniqueness

Signed rationalssrc/rainbow/math/rational/signed/limit_uniqueness.clj0 definitions, 4 theorems

Uniqueness of limits for the signed-rational epsilon-N convergence predicate. The reusable Archimedean lemma says that signed rationals lying in every positive reciprocal band are equivalent. It reduces the two sides of each signed band to nnrat bounds and applies nnrat/at-most-of-all-plus-reciprocal in both directions. For limit uniqueness, at reciprocal radius r the first convergence supplies an r-band around L. The second convergence is instantiated at signed zero, making the common sequence term order-equivalent to L'. Transitivity therefore puts L' in the r-band around L, and the signed Archimedean lemma finishes the proof. Native, axiom-free, and built on the D63 signed convergence/order and nnrat Archimedean toolkits.

Depends onmath.rational.nnrat.archimedeanmath.rational.signed.order-respectsmath.rational.nnrat.identities

signed/add-zero-right :
  (value : ℚ)
  → value + 0 = value

signed/at-most-antisymmetric :
  (a b : ℚ)
  (ab : a ≤ b)
  (ba : b ≤ a)
  → a = b

analysis/equivalent-of-reciprocal-close :
  (x y : ℚ)
  (bounded : ∀ (k : ℕ), analysis/close x (signed/from-nnrat (nnrat/make 1 k)) y)
  → x = y

analysis/limit-unique :
  (s : ℕ → ℚ) (L L-prime : ℚ) (M M-prime : ℚ → ℕ) (to-L : analysis/converges s L M)
  (to-L-prime : analysis/converges s L-prime M-prime)
  → L = L-prime