withDensityᵥ_sub — Mathlib

English

If f and g are integrable, then μ.withDensityᵥ (f - g) equals μ.withDensityᵥ f minus μ.withDensityᵥ g.

Русский

Если f и g интегрируемы, тогда μ.withDensityᵥ (f - g) равен разности μ.withDensityᵥ f и μ.withDensityᵥ g.

LaTeX

$$$ μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g $$$

Lean4

@[simp]
theorem withDensityᵥ_sub (hf : Integrable f μ) (hg : Integrable g μ) :
    μ.withDensityᵥ (f - g) = μ.withDensityᵥ f - μ.withDensityᵥ g := by
  rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]

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