integral_complex_ofReal — Mathlib

English

For a real-valued function f: X → ℝ, the integrals into ℂ coincide: ∫_X (f(x) : ℂ) dμ = ∫_X f(x) dμ as a complex number.

Русский

Для функции f: X → ℝ интеграл в комплексном числе совпадает с комплексным отображением: ∫ (f(x) : ℂ) dμ = ∫ f(x) dμ.

LaTeX

$$$\\int_X (f(x) : \\mathbb{C}) \\,d\\mu = \\int_X f(x) \\,d\\mu$$$

Lean4

theorem integral_complex_ofReal {f : X → ℝ} : ∫ x, (f x : ℂ) ∂μ = ∫ x, f x ∂μ :=
  integral_ofReal

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