integral_im — Mathlib

English

If f: X → 𝕜 is integrable, then the integral commutes with the imaginary part: ∫ Im(f) dμ = Im(∫ f dμ).

Русский

Пусть f: X → 𝕜 интегрируема. Тогда интеграл и мнимая часть коммутируют: ∫ Im(f) dμ = Im(∫ f dμ).

LaTeX

$$$\\int_X \\operatorname{Im}(f(x)) \\,d\\mu = \\operatorname{Im}\\left(\\int_X f(x) \\,d\\mu\\right)$$$

Lean4

theorem integral_im {f : X → 𝕜} (hf : Integrable f μ) : ∫ x, RCLike.im (f x) ∂μ = RCLike.im (∫ x, f x ∂μ) :=
  (@RCLike.imCLM 𝕜 _).integral_comp_comm hf

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