restrict_sInf_eq_sInf_restrict — Mathlib

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]

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