English
Let f: α → 𝕜 and c ∈ 𝕜. The series HasSum f c L is equivalent to the conjunction of HasSum of the real parts to Re(c) and HasSum of the imaginary parts to Im(c): HasSum f c L ↔ HasSum (Re f) Re(c) L ∧ HasSum (Im f) Im(c) L.
Русский
Пусть f: α → 𝕜 и c ∈ 𝕜. Ряд имеет сумму c тогда и только тогда, когда сумма вещественной и мнимой частей даёт соответствующие части c.
LaTeX
$$$ HasSum f c L \\iff HasSum (\\lambda a, \\operatorname{Re}(f(a))) (\\operatorname{Re}(c)) L \\wedge HasSum (\\lambda a, \\operatorname{Im}(f(a))) (\\operatorname{Im}(c)) L $$$
Lean4
theorem hasSum_iff (f : α → 𝕜) (c : 𝕜) :
HasSum f c L ↔ HasSum (fun x => re (f x)) (re c) L ∧ HasSum (fun x => im (f x)) (im c) L :=
by
refine ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, ?_⟩
rintro ⟨h₁, h₂⟩
simpa only [re_add_im] using ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)
