withDensityᵥ_sub' — Mathlib

English

An alias for withDensityᵥ_sub: linearity holds for subtraction.

Русский

Алиас к withDensityᵥ_sub: линейность сохраняется для вычитания.

LaTeX

$$$ withDensityᵥ\\_sub' (hf : Integrable f μ) (hg : Integrable g μ) : μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g $$$

Lean4

theorem withDensityᵥ_sub' (hf : Integrable f μ) (hg : Integrable g μ) :
    (μ.withDensityᵥ fun x => f x - g x) = μ.withDensityᵥ f - μ.withDensityᵥ g :=
  withDensityᵥ_sub hf hg

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