tsum_mul_left — Mathlib

English

In a complete real-topological setting, ∑' i, a * f i = a * ∑' i, f i (for suitable a).

Русский

В надлежащей топологии действительных чисел выполняется ∑' i, a · f(i) = a · ∑' i, f(i).

LaTeX

$$$\text{tsum}_{i\in L}(a \cdot f(i)) = a \cdot \text{tsum}_{i\in L}(f(i))$$$

Lean4

protected theorem tsum_mul_left (a) (hf : Summable f L) : ∑'[L] i, a * f i = a * ∑'[L] i, f i :=
  (hf.hasSum.mul_left _).tsum_eq

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