Theorems · Theorem · order theory

Finset.sum_lt_sum

∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {f g : ι → M} {s : Finset ι} [AddLeftStrictMono M],
  (∀ i ∈ s, f i ≤ g i) → (∃ i ∈ s, f i < g i) → ∑ i ∈ s, f i < ∑ i ∈ s, g i

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

11 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidPreorderIsOrderedCancelAddMonoidAddLeftStrictMono