Reference · Signed rationals

rainbow.math.rational.signed.order-monotone

Signed rationalssrc/rainbow/math/rational/signed/order_monotone.clj0 definitions, 3 theorems

Real-analysis roadmap step 6a: signed order is monotone under addition -- signed/add-right-monotone : a <= b -> (a + c) <= (b + c) signed/add adds pos/neg componentwise (pos(a+c) = pos a + pos c, etc. -- reduces definitionally, since signed/positive-of-make is reflexivity), so the goal (Pa+Pc)+(Nb+Nc) <= (Pb+Pc)+(Na+Nc) reorders (nnrat/add-four-reorder) to (Pa+Nb)+(Pc+Nc) <= (Pb+Na)+(Pc+Nc) which is nnrat/add-monotone applied to the hypothesis Pa+Nb <= Pb+Na with the common (Pc+Nc) (at-most-reflexive), transported back by nnrat/at-most-respects-equivalence. A building block for 'L <= L + eps' and the limit laws. Native and axiom-free; chains rainbow.math.rational.signed.order-transitivity (-> nnrat add-monotone, four-reorder) on d63.

Depends onmath.rational.signed.order-transitivity

signed/add-right-monotone :
  (a b c : ℚ)
  (ha : a ≤ b)
  → a + c ≤ b + c

signed/add-left-monotone :
  (a b c : ℚ)
  (ha : a ≤ b)
  → c + a ≤ c + b

signed/add-monotone :
  (a ah b bh : ℚ)
  (ha : a ≤ ah)
  (hb : b ≤ bh)
  → a + b ≤ ah + bh