hasSum_re — Mathlib

English

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

Русский

Если f: α → ℂ имеет сумму x, то сумма вещественных частей равна вещественной части суммы: HasSum (a ↦ Re(f(a))) Re(x) L.

LaTeX

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

Lean4

theorem hasSum_re {f : α → ℂ} {x : ℂ} (h : HasSum f x L) : HasSum (fun x => (f x).re) x.re L :=
  RCLike.hasSum_re ℂ h

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