tsum_iUnion_le — Mathlib

English

If ι is finite, then the sum over the union iUnion t_i is ≤ the sum over i of the sums over t_i.

Русский

Если ι конечен, то сумма по iUnion 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_iUnion_le {ι : Type*} [Fintype ι] (f : α → ℝ≥0∞) (t : ι → Set α) :
    ∑' x : ⋃ i, t i, f x ≤ ∑ i, ∑' x : t i, f x :=
  by
  rw [← tsum_fintype (L := SummationFilter.unconditional _)]
  exact tsum_iUnion_le_tsum f t

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