Reference · Non-negative rationals

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

Non-negative rationalssrc/rainbow/math/rational/nnrat/map_sum_respects.clj0 definitions, 1 theorems

map-sum is a congruence for pointwise nnrat equivalence: nnrat/map-sum-respects-equivalence : (forall i, f i ~ g i) -> map-sum f is ~ map-sum g is Lets a per-term equivalence be rewritten underneath a finite sum -- the tool that applies map-sum-scale-right (and the per-term product reorder) inside the LP double sum. List.rec induction: nil is reflexivity; cons is add-respects-equivalence on the head equivalence (hypothesis) and the tail equivalence (IH). Polymorphic in the element type. Native and axiom-free; chains nnrat-list-sum on d63.

Depends onmath.rational.nnrat.list-sum

nnrat/map-sum-respects-equivalence.{u} :
  (A : Type u) (f g : A → ℚ≥0)
  (hfg : ∀ (i : A), f i = g i)
  (is : List A)
  → nnrat/map-sum A f is = nnrat/map-sum A g is