restrict_withDensity' — Mathlib

English

Under SFinite μ, the same restriction-with-density equality holds for any set s.

Русский

При MS конечной по μ равенство ограничения с плотностью сохраняется для любого множества s.

LaTeX

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

Lean4

theorem restrict_withDensity' [SFinite μ] (s : Set α) (f : α → ℝ≥0∞) :
    (μ.withDensity f).restrict s = (μ.restrict s).withDensity f :=
  by
  ext1 t ht
  rw [restrict_apply ht, withDensity_apply _ ht, withDensity_apply' _ (t ∩ s), restrict_restrict ht]

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