tsum_prod' — Mathlib

English

The same product-sum decompositions hold for functions f : α × β → ENNReal, i.e., ∑' p ∈ α×β f(p) = ∑' 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 = ∑' (a) (b), f (a, b) :=
  ENNReal.summable.tsum_prod' fun _ => ENNReal.summable

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