English
For [L.NeBot], if f: α → ℂ is summable, then the real part of the tsum equals the tsum of the real parts: Re( tsum f L ) = tsum (Re f) L.
Русский
При условии L NeBot, если f: α → ℂ сходится, то вещественная часть суммы равна сумме вещественных частей: Re( tsum f L ) = tsum (Re f) L.
LaTeX
$$$ [L.NeBot] \\; \\{f : α \\to \\mathbb{C}\\} \\Rightarrow \\operatorname{Re}\\Bigl( \\sum'[L] a, f(a) \\Bigr) = \\sum'[L] a, \\operatorname{Re}(f(a)) $$$
Lean4
theorem re_tsum [L.NeBot] {f : α → ℂ} (h : Summable f L) : (∑'[L] a, f a).re = ∑'[L] a, (f a).re :=
RCLike.re_tsum _ h