tsum_eval — Mathlib

English

If p is summable, then summing p over a and evaluating at m equals evaluating the sum at m.

Русский

Если p суммируема, то суммирование p(a) по a и последующая оценка в m равны оценке суммы в m.

LaTeX

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

Lean4

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

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