Reference · Non-negative rationals

rainbow.math.rational.nnrat.lattice-monotone

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

Universal monotonicity of the exact-rational min and max under the rational order, composing the min/max bound + lattice-step theorems from rainbow.math.rational.nnrat.minmax: min-monotone : a<=a' -> b<=b' -> min a b <= min a' b' max-monotone : a<=a' -> b<=b' -> max a b <= max a' b' i.e. improving both arguments never lowers the min or the max. These upgrade to universal the pointwise-dominance behaviour the AHoF catalog exercised on worked instances for min/max aggregation (robust worst-case max, bottleneck/min-cost, clipping, monitor envelopes). Each proof lifts the endpoints through nnrat/at-most-transitive into the greatest-lower-bound (minmax/at-most-min) or least-upper-bound (minmax/at-most-max) step. Native and axiom-free; chains rainbow.math.rational.nnrat.minmax (on the d63 base).

Depends onmath.rational.nnrat.minmax

minmax/min-monotone :
  (a a-hi b b-hi : ℚ≥0)
  (ha : a ≤ a-hi)
  (hb : b ≤ b-hi)
  → minmax/min a b ≤ minmax/min a-hi b-hi

minmax/max-monotone :
  (a a-hi b b-hi : ℚ≥0)
  (ha : a ≤ a-hi)
  (hb : b ≤ b-hi)
  → minmax/max a b ≤ minmax/max a-hi b-hi