apply_union_le_sum — Mathlib

English

For an additive monoid setup and a function f on sets, the value at the union is bounded by the sum of values on the pieces: f(⋃ i∈t, s i) ≤ ∑_{i∈t} f(s i).

Русский

В дополнение к суммированию по элементам, значение на объединении ≤ сумма значений по частям: f(⋃ i∈t s i) ≤ ∑_{i∈t} f(s i).

LaTeX

$$$f\left(\bigcup_{i\in t} s(i)\right) \le \sum_{i\in t} f(s(i))$$$

Lean4

theorem apply_union_le_sum [AddCommMonoid β] [PartialOrder β] [AddLeftMono β] {f : Set α → β} (zero : f ∅ = 0)
    (ih : ∀ {s t}, f (s ∪ t) ≤ f s + f t) {s : ι → Set α} (t : Finset ι) : f (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, f (s i) :=
  Finset.sup_set_eq_biUnion t s ▸ t.apply_sup_le_sum zero (by simpa)

Похожие утверждения