intervalIntegral_ofReal — Mathlib

English

For 𝕜 with RCLike structure, ∫ (f x) over a..b in 𝕜 equals the same integral of f over a..b in the real numbers, mapped to 𝕜.

Русский

Для 𝕜 с RCLike структурой интеграл от f на a..b в 𝕜 равен интегралу в реальных числах, отображённому в 𝕜.

LaTeX

$$$\int_{a}^{b} f(x) \, dμ\; (in\; 𝕜) = \text{ofReal}\left( \int_{a}^{b} f(x) \, dμ\; (in\; \mathbb{R}) \right)$$$

Lean4

nonrec theorem _root_.RCLike.intervalIntegral_ofReal {𝕜 : Type*} [RCLike 𝕜] {a b : ℝ} {μ : Measure ℝ} {f : ℝ → ℝ} :
    (∫ x in a..b, (f x : 𝕜) ∂μ) = ↑(∫ x in a..b, f x ∂μ) := by
  simp only [intervalIntegral, integral_ofReal, RCLike.ofReal_sub]

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