tsum_apply — Mathlib

English

The sum over a family of functions commutes with evaluation: the sum over i of f(i) evaluated at x equals the sum over i of f(i)(x).

Русский

Сумма по семейству функций является функцией, получаемой суммой по значениям: сумма по i от f(i), примененная к x, равна сумме по i от f(i)(x).

LaTeX

$$$(\sum' i, f(i))\; x = \sum' i, f(i)\,x.$$$

Lean4

protected theorem tsum_apply {ι α : Type*} {f : ι → α → ℝ≥0∞} {x : α} : (∑' i, f i) x = ∑' i, f i x :=
  tsum_apply <| Pi.summable.mpr fun _ => ENNReal.summable

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