re_tsum — Mathlib

English

If f: α → 𝕜 is summable, then the real part of the tsum equals the tsum of the real parts: Re(∑'[L] a, f(a)) = ∑'[L] a, Re(f(a)).

Русский

Если f: α → 𝕜 сходится, то действительная часть суммы равна сумме действительных частей: Re(∑ f(a)) = ∑ Re(f(a)).

LaTeX

$$$ \\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) : re (∑'[L] a, f a) = ∑'[L] a, re (f a) :=
  reCLM.map_tsum h

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