integral_conj — Mathlib

English

If f: X → 𝕜 is integrable, then the integral commutes with complex conjugation: ∫ conj(f(x)) dμ = conj(∫ f(x) dμ).

Русский

Пусть f: X → 𝕜 интегрируема. Тогда интеграл сопряжённого совпадает с сопряжённым интеграла: ∫ conj(f(x)) dμ = conj(∫ f(x) dμ).

LaTeX

$$$\\int_X \\overline{f(x)} \\,d\\mu = \\overline{\\int_X f(x) \\,d\\mu}$$$

Lean4

theorem integral_conj {f : X → 𝕜} : ∫ x, conj (f x) ∂μ = conj (∫ x, f x ∂μ) :=
  (@RCLike.conjLIE 𝕜 _).toLinearIsometry.integral_comp_comm f

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