integral_const_mul — Mathlib

English

For 𝕜 with RCLike structure and real-valued f, the interval integral commutes with the real-to-𝕜 embedding: ∫ (f x) in 𝕜 = ofReal (∫ f x in ℝ).

Русский

Для 𝕜 с структурой RCLike и вещественной функции f интеграл по интервалу согласуется с вложением вещественного в 𝕜: ∫ (f x) в 𝕜 = ofReal (∫ f x).

LaTeX

$$$\int_{a}^{b} (f(x) : 𝕜) \, dμ = \uparrow\left( \int_{a}^{b} f(x) \, dμ \right)$$$

Lean4

@[simp]
theorem integral_const_mul [NormedDivisionRing 𝕜] [NormedAlgebra ℝ 𝕜] (r : 𝕜) (f : ℝ → 𝕜) :
    ∫ x in a..b, r * f x ∂μ = r * ∫ x in a..b, f x ∂μ :=
  integral_smul r f

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