tsum_biUnion' — Mathlib

English

For S a set of indices with pairwise disjoint t_i, the total sum over the union equals the supremum over i of the sums over t_i.

Русский

Для множества индексов S с попарно непересекающимися t_i: общая сумма по объединению равна верхней границе сумм по каждому t_i.

LaTeX

$$$\\sum' x : \\bigcup_{i \\in S} t_i, f(x) = \\bigl(\\sum' i : S, \\sum' x : t_i, f(x)\\bigr).$$$

Lean4

protected theorem tsum_biUnion' {ι : Type*} {S : Set ι} {f : α → ENNReal} {t : ι → Set α} (h : S.PairwiseDisjoint t) :
    ∑' x : ⋃ i ∈ S, t i, f x = ∑' (i : S), ∑' (x : t i), f x := by
  simp [← ENNReal.tsum_sigma, ← (Set.biUnionEqSigmaOfDisjoint h).tsum_eq]

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