withDensityᵥ_neg' — Mathlib

English

The withDensityᵥ construction commutes with negation in the sense that withDensityᵥ(-f) equals the negation of withDensityᵥ(f).

Русский

Конструкция withDensityᵥ корректно обращается с отрицанием: withDensityᵥ(-f) = - withDensityᵥ(f).

LaTeX

$$$ \\mu.withDensityᵥ(-f) = -\\mu.withDensityᵥ(f) $$$

Lean4

theorem withDensityᵥ_neg' : (μ.withDensityᵥ fun x => -f x) = -μ.withDensityᵥ f :=
  withDensityᵥ_neg

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