integral_ofReal — Mathlib

English

The interval integral commutes with the real-to-Real embedding, i.e., integral of Real into Real via the canonical embedding equals the same Real integral.

Русский

Интеграл по интервалу коммутирует с отображением Real в Real через каноническое вложение, т.е. тот же интеграл.

LaTeX

$$$\int_{a}^{b} (f(x) : ℝ) \, dμ = (\int_{a}^{b} f(x) \, dμ)$$$

Lean4

nonrec theorem integral_ofReal {a b : ℝ} {μ : Measure ℝ} {f : ℝ → ℝ} :
    (∫ x in a..b, (f x : ℂ) ∂μ) = ↑(∫ x in a..b, f x ∂μ) :=
  RCLike.intervalIntegral_ofReal

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