withDensityᵥ_add' — Mathlib

English

An alias for withDensityᵥ_add: the same linearity holds for integrable f and g.

Русский

Алиас к withDensityᵥ_add: та же линейность для интегрируемых f и g.

LaTeX

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

Lean4

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

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