Theorems · Theorem · order theory

Finset.apply_prod_le_sum_apply

∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [AddLeftMono β] (s : Finset ι) {f : ι → α} (g : α → β),
  g 1 ≤ 0 → (∀ (a b : α), g (a * b) ≤ g a + g b) → g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

4 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

CommMonoidAddCommMonoidPreorderAddLeftMono