tsum_comm — Mathlib

English

For any f : α → β → ENNReal, the order of summation can be swapped: ∑' a, ∑' b, f(a,b) = ∑' b, ∑' a, f(a,b).

Русский

Для любой функции f : α → β → ENNReal сумма можно переставлять: ∑'_a ∑'_b f(a,b) = ∑'_b ∑'_a f(a,b).

LaTeX

$$$\sum'_{a \in \alpha} \sum'_{b \in \beta} f(a,b) = \sum'_{b \in \beta} \sum'_{a \in \alpha} f(a,b)$$$

Lean4

protected theorem tsum_comm {f : α → β → ℝ≥0∞} : ∑' a, ∑' b, f a b = ∑' b, ∑' a, f a b :=
  ENNReal.summable.tsum_comm' (fun _ => ENNReal.summable) fun _ => ENNReal.summable

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