integral_re — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem integral_re {f : X → 𝕜} (hf : Integrable f μ) : ∫ x, RCLike.re (f x) ∂μ = RCLike.re (∫ x, f x ∂μ) :=
  (@RCLike.reCLM 𝕜 _).integral_comp_comm hf

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