hasSum_im — Mathlib

English

If f: α → 𝕜 has sum x, then the imaginary parts also sum to the imaginary part of x: HasSum (a ↦ Im(f(a))) (Im x) L.

Русский

Если f: α → 𝕜 имеет сумму x, то мнимая часть суммы равна мнимой части x: HasSum (a ↦ Im(f(a))) (Im x) L.

LaTeX

$$$ HasSum\\bigl(a \\mapsto \\operatorname{Im}(f(a))\\bigr) \\; \\operatorname{Im}(x) \\; L $$$

Lean4

theorem hasSum_im {f : α → 𝕜} {x : 𝕜} (h : HasSum f x L) : HasSum (fun x => im (f x)) (im x) L :=
  imCLM.hasSum h

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