tsum_sigma — Mathlib

English

For f : α → β → ENNReal, the double sum over Σ a, β a equals the iterated sums via Sigma construction: ∑' p, f p = ∑' a ∑' b, f a b.

Русский

Для f(a,b) равенство двойной суммы через сигма-конструкцию.

LaTeX

$$$\\sum' p : \\Sigma a, b, f(p.fst,p.snd) = \\sum' a, \\sum' b, f(a,b).$$$

Lean4

protected theorem tsum_sigma {β : α → Type*} (f : ∀ a, β a → ℝ≥0∞) : ∑' p : Σ a, β a, f p.1 p.2 = ∑' (a) (b), f a b :=
  ENNReal.summable.tsum_sigma' fun _ => ENNReal.summable

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