restrict_trim — Mathlib

English

The restriction of the trimmed measure to a set s equals the trimmed restriction: (μ.trim hm).restrict s = (μ.restrict s).trim hm.

Русский

Ограничение обрезанной меры на множество s равно обрезке ограниченной меры: (μ.trim hm).restrict s = (μ.restrict s).trim hm.

LaTeX

$$$(μ.Trim hm).restrict s = (μ.restrict s).trim hm.$$$

Lean4

theorem restrict_trim (hm : m ≤ m0) (μ : Measure α) (hs : @MeasurableSet α m s) :
    @Measure.restrict α m (μ.trim hm) s = (μ.restrict s).trim hm :=
  by
  refine @Measure.ext _ m _ _ (fun t ht => ?_)
  rw [@Measure.restrict_apply α m _ _ _ ht, trim_measurableSet_eq hm ht, Measure.restrict_apply (hm t ht),
    trim_measurableSet_eq hm (@MeasurableSet.inter α m t s ht hs)]

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