im_tsum — Mathlib

English

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

Русский

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

LaTeX

$$$ \\operatorname{Im}\\Bigl( \\sum'[L] a, f(a) \\Bigr) = \\sum'[L] a, \\operatorname{Im}(f(a)) $$$

Lean4

theorem im_tsum [L.NeBot] {f : α → 𝕜} (h : Summable f L) : im (∑'[L] a, f a) = ∑'[L] a, im (f a) :=
  imCLM.map_tsum h

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