tsum_sigma' — Mathlib

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

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