Theorems · Theorem · order theory

Finset.sum_le_sum

∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f g : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, f i ≤ g i) → ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i

In an ordered additive commutative monoid, if each summand f i of one finite sum is less than or equal to the corresponding summand g i of another finite sum, then ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i.

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

182 results in Mathlib

Foundations

Depth 54 from the axioms, rests on 859 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidPreorderAddLeftMono