tsum_eval — Mathlib

English

Summing a summable family of multilinear maps commutes with evaluation.

Русский

Сумма суммируемой семьи много-линейных отображений коммутирует с оцениванием.

LaTeX

$$$\\text{Summable}(p) \\Rightarrow (\\sum' a, p(a))\\,m = \\sum' a, p(a)(m)$$$

Lean4

theorem tsum_eval [T2Space F] {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F} (hp : Summable p) (m : Π i, E i) :
    (∑' a, p a) m = ∑' a, p a m :=
  (hasSum_eval hp.hasSum m).tsum_eq.symm

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