integral_const' — Mathlib

English

For c ∈ ℝ≥0∞, the integral over a..b of f with c • μ equals c.toReal times the integral of f.

Русский

Для c ∈ ℝ≥0∞ интеграл ∫ f по a..b с мерой c • μ равен c.toReal умноженному на интеграл ∫ f.

LaTeX

$$$\int_{a}^{b} f(x) \, d(c \cdot μ) = c.toReal \cdot \int_{a}^{b} f(x) \, dμ$$$

Lean4

theorem integral_const' [CompleteSpace E] (c : E) : ∫ _ in a..b, c ∂μ = (μ.real (Ioc a b) - μ.real (Ioc b a)) • c := by
  simp only [measureReal_def, intervalIntegral, setIntegral_const, sub_smul]

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