hasSum_iff — Mathlib

English

For f: α → ℂ and c ∈ ℂ, HasSum f c L holds iff both HasSum (a ↦ Re(f(a))) (Re c) L and HasSum (a ↦ Im(f(a))) (Im c) L hold.

Русский

Для f: α → ℂ и c ∈ ℂ имеет место эквивалентность: HasSum f c = HasSum Re(f) Re(c) и HasSum Im(f) Im(c).

LaTeX

$$$ HasSum f c L \\iff \\bigl( HasSum (a \\mapsto \\operatorname{Re}(f(a))) (\\operatorname{Re}(c)) L \\wedge HasSum (a \\mapsto \\operatorname{Im}(f(a))) (\\operatorname{Im}(c)) L \\bigr) $$$

Lean4

theorem hasSum_iff (f : α → ℂ) (c : ℂ) :
    HasSum f c L ↔ HasSum (fun x => (f x).re) c.re L ∧ HasSum (fun x => (f x).im) c.im L :=
  RCLike.hasSum_iff _ _

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