English
The restriction of an infimum of a collection of measures equals the infimum of the restricted measures.
Русский
ОграничениеInf коллекции мер равно Inf ограничений.
LaTeX
$$$(sInf\, m).restrict t = sInf (\{ μ.restrict t : μ ∈ m \})$$$
Lean4
/-- This lemma shows that `Inf` and `restrict` commute for measures. -/
theorem restrict_sInf_eq_sInf_restrict {m0 : MeasurableSpace α} {m : Set (Measure α)} (hm : m.Nonempty)
(ht : MeasurableSet t) : (sInf m).restrict t = sInf ((fun μ : Measure α => μ.restrict t) '' m) :=
by
ext1 s hs
simp_rw [sInf_apply hs, restrict_apply hs, sInf_apply (MeasurableSet.inter hs ht), Set.image_image,
restrict_toOuterMeasure_eq_toOuterMeasure_restrict ht, ← Set.image_image _ toOuterMeasure, ←
OuterMeasure.restrict_sInf_eq_sInf_restrict _ (hm.image _), OuterMeasure.restrict_apply]