withDensity_add_right — Mathlib

English

If g is measurable, then μ.withDensity (f+g) = μ.withDensity f + μ.withDensity g.

Русский

Если g измерима, то μ.withDensity (f+g) = μ.withDensity f + μ.withDensity g.

LaTeX

$$$g \text{ measurable} \Rightarrow \mu.withDensity (f+g) = \mu.withDensity f + \mu.withDensity g$$$

Lean4

theorem withDensity_add_right (f : α → ℝ≥0∞) {g : α → ℝ≥0∞} (hg : Measurable g) :
    μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g := by
  simpa only [add_comm] using withDensity_add_left hg f

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