English
If μ is an outer measure and s is measurable, then restricting to s after trimming equals trimming after restricting.
Русский
Пусть μ — внешняя мера, s измерима. Тогда ограничение к s после обрезки равно обрезке после ограничения.
LaTeX
$$$(\\mathrm{restrict}\\; s\\; \\mu)^{\\mathrm{trim}} = \\mathrm{restrict}\\; s\\; (\\mu^{\\mathrm{trim}}).$$$
Lean4
/-- The trimmed property of a measure μ states that `μ.toOuterMeasure.trim = μ.toOuterMeasure`.
This theorem shows that a restricted trimmed outer measure is a trimmed outer measure. -/
theorem restrict_trim {μ : OuterMeasure α} {s : Set α} (hs : MeasurableSet s) :
(restrict s μ).trim = restrict s μ.trim :=
by
refine le_antisymm (fun t => ?_) (le_trim_iff.2 fun t ht => ?_)
· rw [restrict_apply]
rcases μ.exists_measurable_superset_eq_trim (t ∩ s) with ⟨t', htt', ht', hμt'⟩
rw [← hμt']
rw [inter_subset] at htt'
refine (measure_mono htt').trans ?_
rw [trim_eq _ (hs.compl.union ht'), restrict_apply, union_inter_distrib_right, compl_inter_self, Set.empty_union]
exact measure_mono inter_subset_left
· rw [restrict_apply, trim_eq _ (ht.inter hs), restrict_apply]
