integral_smul_const — Mathlib

English

If f: ℝ → E and r ∈ 𝕜, then ∫ f(x) · r = (∫ f(x)) · r.

Русский

Если f: ℝ → E и r ∈ 𝕜, то ∫ f(x) · r = (∫ f(x)) · r.

LaTeX

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

Lean4

@[simp]
nonrec theorem integral_smul_const [CompleteSpace E] {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ℝ → 𝕜) (c : E) :
    ∫ x in a..b, f x • c ∂μ = (∫ x in a..b, f x ∂μ) • c := by
  simp only [intervalIntegral_eq_integral_uIoc, integral_smul_const, smul_assoc]

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