withDensityᵥ_smul' — Mathlib

English

An alias for withDensityᵥ_smul: the same equality holds for smul on the integrand.

Русский

Псевдоним к withDensityᵥ_smul: та же равенство справедлива для smul в интегране.

LaTeX

$$$ withDensityᵥ\\_smul' (f : α → E) (r : 𝕜) : μ.withDensityᵥ (r \\cdot f) = r \\cdot μ.withDensityᵥ f $$$

Lean4

theorem withDensityᵥ_smul' {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℝ 𝕜 E] (f : α → E)
    (r : 𝕜) : (μ.withDensityᵥ fun x => r • f x) = r • μ.withDensityᵥ f :=
  withDensityᵥ_smul f r

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