rainbow.math.rational.nnrat.map-sum-on

Non-negative rationals src/rainbow/math/rational/nnrat/map_sum_on.clj0 definitions, 1 theorems

Compatibility entry point for the canonical member-restricted sum theorem. Master's metric-separation installer is authoritative. The independently written proof is retained only as a kernel-checked test fixture.

Depends onmath.rational.nnrat.metric-separation

nnrat/map-sum-monotone-on

TheoremFor all inputsNo axiomsSource

nnrat/map-sum-monotone-on.{u} :
  (A : Type u) (f g : A → ℚ≥0) (items : List A)
  (bounded : ∀ (value : A), ∀ (member : list/membership A items value), f value ≤ g value)
  → nnrat/map-sum A f items ≤ nnrat/map-sum A g items

List = data/Listℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most