integral_smul — Mathlib

English

For c ∈ 𝕜 and f ∈ α →₁ₛ[μ] E, the integral commutes with scalar multiplication: ∫ (c • f) dμ = c • ∫ f dμ.

Русский

Для скаляра c и f интеграл коммутирует с умножением на скаляр: ∫ (c • f) dμ = c • ∫ f dμ.

LaTeX

$$$\int (c \cdot f) \, d\mu = c \cdot \int f \, d\mu$$$

Lean4

theorem integral_smul (c : 𝕜) (f : α →₁ₛ[μ] E) : integral (c • f) = c • integral f :=
  setToL1S_smul _ (fun _ _ => weightedSMul_null) weightedSMul_union weightedSMul_smul c f

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