tsum_biUnion_le — Mathlib

English

For a finite index set, the sum over the union of t_i is ≤ the sum over i of the sums over t_i.

Русский

Для конечного множества индексов сумма по объединению 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 {ι : Type*} (f : α → ℝ≥0∞) (s : Finset ι) (t : ι → Set α) :
    ∑' x : ⋃ i ∈ s, t i, f x ≤ ∑ i ∈ s, ∑' x : t i, f x :=
  (tsum_biUnion_le_tsum f s.toSet t).trans_eq (Finset.tsum_subtype s fun i => ∑' x : t i, f x)

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