tsum_prod — Mathlib

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

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