tsum_add — Mathlib

English

For any f,g : α → ENNReal, the sum distributes over addition inside the summation: ∑' a, (f(a) + g(a)) = (∑' a, f(a)) + (∑' a, g(a)).

Русский

Сумма распадается по сложению внутри суммирования: ∑'_a (f(a) + g(a)) = (∑'_a f(a)) + (∑'_a g(a)).

LaTeX

$$$\sum'_{a \in \alpha} (f(a) + g(a)) = \left(\sum'_{a \in \alpha} f(a)\right) + \left(\sum'_{a \in \alpha} g(a)\right)$$$

Lean4

protected theorem tsum_add : ∑' a, (f a + g a) = ∑' a, f a + ∑' a, g a :=
  ENNReal.summable.tsum_add ENNReal.summable

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