tsum_mul_left — Mathlib

English

Multiplication by a fixed nonnegative real on the left commutes with summation: the sum of a scaled family equals the scale times the sum.

Русский

Умножение всей серии на константу слева сохраняет сумму: сумма константы на множителе равно константе, умноженной на сумму.

LaTeX

$$$\\sum\\'_{L} x\\,(a\\cdot f(x)) = a\\cdot \\sum\\'_{L} x\\, f(x)\\quad (a\\in\\mathbb{R}_{\\ge 0})$$$

Lean4

nonrec theorem tsum_mul_left (a : ℝ≥0) (f : α → ℝ≥0) : ∑'[L] x, a * f x = a * ∑'[L] x, f x :=
  NNReal.eq <| by simp only [coe_tsum, NNReal.coe_mul, tsum_mul_left]

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