Theorems · Theorem · order theory

Finset.le_sum_of_subadditive_on_pred

∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] [inst_2 : Preorder N]
  [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop),
  f 0 ≤ 0 →
    (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) →
      (∀ (x y : M), p x → p y → p (x + y)) →
        ∀ (g : ι → M) {s : Finset ι}, (∀ i ∈ s, p (g i)) → f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

Let {x | p x} be a subsemigroup of a commutative additive monoid M. Let f : M → N be a map such that f 0 = 0 and f is subadditive on {x | p x}, i.e. p x → p y → f (x + y) ≤ f x + f y. Let g i, i ∈ s, be a finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ x ∈ s, g x) ≤ ∑ x ∈ s, f (g x).

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidPreorderIsOrderedAddMonoid