Reference · Non-negative rationals

rainbow.math.rational.nnrat.multiply-right-monotone

Non-negative rationalssrc/rainbow/math/rational/nnrat/multiply_right_monotone.clj0 definitions, 2 theorems

Right-factor monotonicity of nnrat multiplication under the rational order: nnrat/multiply-right-monotone : a <= b -> (a * c) <= (b * c) The mirror of rainbow.math.rational.nnrat.multiply-monotone (left factor). Same technique: the base lemma reduces base(a*c)(b*c) to a nat cross-product, regroups both sides with nat/multiply-four-reorder into (na*db)*(nc*dc) <= (nb*da)*(nc*dc), applies nat/multiply-RIGHT-monotone to the hypothesis, and transports the packed product denominators via the nnrat/denominator-combine law; the full theorem lifts across the reflexive-transitive closure nnrat/at-most. Needed for factor-comparison results (e.g. gamma <= 1/2 -> gamma*x <= (1/2)*x), which generalise contraction convergence beyond the 1/2 rate. Native and axiom-free; self-contained on d63.

nnrat/multiply-right-monotone-base :
  (a b c : ℚ≥0) (h : nnrat/base-at-most a b)
  → nnrat/base-at-most (a · c) (b · c)

nnrat/multiply-right-monotone :
  (a b c : ℚ≥0)
  (h : a ≤ b)
  → a · c ≤ b · c