tsum_biUnion_le_tsum — Mathlib

English

For a family of sets t_i and a function f, the sum over the union ∪i t_i is ≤ the sum over i of the sums over t_i.

Русский

Сумма по объединению множеств ≤ сумма по i от сумм по каждому t_i.

LaTeX

$$$\sum' x : \bigcup_i t_i, f(x) \le \sum_i \sum' x : t_i, f(x).$$$

Lean4

theorem tsum_biUnion_le_tsum {ι : Type*} (f : α → ℝ≥0∞) (s : Set ι) (t : ι → Set α) :
    ∑' x : ⋃ i ∈ s, t i, f x ≤ ∑' i : s, ∑' x : t i, f x :=
  calc
    ∑' x : ⋃ i ∈ s, t i, f x = ∑' x : ⋃ i : s, t i, f x := tsum_congr_set_coe _ <| by simp
    _ ≤ ∑' i : s, ∑' x : t i, f x := tsum_iUnion_le_tsum _ _

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