restrict_withDensity — Mathlib

English

The restriction of μ with density f to a measurable set s equals the density of the restricted μ to s.

Русский

Ограничение μ с плотностью f на измеримое множество s равно плотности ограниченной μ на s.

LaTeX

$$ (μ.withDensity f).restrict s = (μ.restrict s).withDensity f $$

Lean4

theorem restrict_withDensity {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    (μ.withDensity f).restrict s = (μ.restrict s).withDensity f :=
  by
  ext1 t ht
  rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply _ (ht.inter hs), restrict_restrict ht]

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