Theorems · Theorem · order theory

Finset.le_sum_nonempty_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),
  (∀ (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 ι), s.Nonempty → (∀ i ∈ s, p (g i)) → f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

Let {x | p x} be an additive subsemigroup of an additive commutative monoid M. Let f : M → N be a map 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 nonempty finite family of elements of M such that ∀ i ∈ s, p (g i). Then f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i).

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddCommMonoidAddCommMonoidPreorderIsOrderedAddMonoid