hasSum_im — Mathlib

English

If f: α → ℂ has sum x ∈ ℂ, then the HasSum of the imaginary parts equals the imaginary part of the sum: HasSum (a ↦ Im(f(a))) Im(x) L.

Русский

Если f: α → ℂ имеет сумму 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 => (f x).im) x.im L :=
  RCLike.hasSum_im ℂ h

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