Theorems · Theorem · order theory

Finset.apply_union_le_sum

∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid β] [inst_1 : Preorder β] [AddLeftMono β]
  {f : Set α → β},
  f ∅ = 0 →
    (∀ {s t : Set α}, f (s ∪ t) ≤ f s + f t) → ∀ {s : ι → Set α} (t : Finset ι), f (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, f (s i)

Defined in

Mathlib.Algebra.Order.BigOperators.Group.Finset

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPreorderAddLeftMono