hasSum_eval — Mathlib

English

If p maps index α to continuous alternating maps and q is its sum, then for any m ∈ E^ι, the sum of p(a) evaluated at m equals q(m).

Русский

Если p выводит индекc α в непрерывные чередующиеся отображения и q является суммой p, то сумма p(a) при m совпадает с q(m).

LaTeX

$$$\\text{HasSum}(p,q) \\Rightarrow \\forall m, \\HasSum(\\lambda a. p(a)(m), q(m))$$$

Lean4

theorem hasSum_eval {α : Type*} {p : α → E [⋀^ι]→L[𝕜] F} {q : E [⋀^ι]→L[𝕜] F} (h : HasSum p q) (m : ι → E) :
    HasSum (fun a => p a m) (q m) :=
  h.map (applyAddHom m) (continuous_eval_const m)

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