tsum_smul_const — Mathlib

English

Duplicate entry: same as previous item, stating Fubini-type product-sum relation for summable families.

Русский

Повтор предыдущего: отношение суммы и произведения для суммируемых семейств

LaTeX

$$$$ (\sum' i, f i) \; \text{smul} \; (\sum' j, g j) = \sum' z : i \times j, f z.1 \cdot g z.2. $$$$

Lean4

protected theorem tsum_smul_const [T2Space M] [L.NeBot] (hf : Summable f L) (a : M) :
    ∑'[L] z, f z • a = (∑'[L] z, f z) • a :=
  (hf.hasSum.smul_const _).tsum_eq

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