English
For a pairwise disjoint family of sets t i over i in S with S a finite-disjoint collection, the sum over the union equals the sum over i of the sums over t i.
Русский
Для попарно неперекрывающихся множеств t i: сумма по объединению равна сумме по i от сумм по каждому t i.
LaTeX
$$$\\sum' x : \\bigcup_{i\\in S} t_i, f(x) = \\sum' i : S, \\sum' x : t_i, f(x).$$$
Lean4
protected theorem tsum_sigma' {β : α → Type*} (f : (Σ a, β a) → ℝ≥0∞) : ∑' p : Σ a, β a, f p = ∑' (a) (b), f ⟨a, b⟩ :=
ENNReal.summable.tsum_sigma' fun _ => ENNReal.summable