hasSum_eval — Mathlib

English

If p sums to q in CM_k(E,F) then evaluating at m preserves the summation, i.e., the sum of p at m equals q at m.

Русский

Если п суммируется к q в CM_k(E,F), то при фиксированном m сумма p на m равна q на m.

LaTeX

$$$\\text{HasSum}(p,q) \\Rightarrow \\forall m, \\; \\sum p(a)(m) = q(m)$$$

Lean4

theorem hasSum_eval {α : Type*} {p : α → ContinuousMultilinearMap 𝕜 E F} {q : ContinuousMultilinearMap 𝕜 E F}
    (h : HasSum p q) (m : Π i, E i) : HasSum (fun a => p a m) (q m) :=
  h.map (applyAddHom m) (continuous_eval_const m)

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