English
For any f : α → β → ENNReal, the sum over the Cartesian product α × β equals the iterated sum: ∑_{p ∈ α×β} f(p.1, p.2) = ∑_{a ∈ α} ∑_{b ∈ β} f(a, b).
Русский
Для любой функции f : α → β → ENNReal сумма по Декартову произведению α × β равна итеративной сумме: ∑_{(a,b) ∈ α×β} f(a,b) = ∑_{a ∈ α} ∑_{b ∈ β} f(a,b).
LaTeX
$$$\sum'_{(a,b) \in \alpha \times \beta} f(a,b) = \sum_{a \in \alpha} \sum_{b \in \beta} f(a,b)$$$
Lean4
protected theorem tsum_prod {f : α → β → ℝ≥0∞} : ∑' p : α × β, f p.1 p.2 = ∑' (a) (b), f a b :=
ENNReal.summable.tsum_prod' fun _ => ENNReal.summable