Theorems · Theorem · order theory

Finset.single_lt_sum

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

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPreorderIsOrderedCancelAddMonoidAddLeftStrictMono