restrict_sInf_eq_sInf_restrict — Mathlib

English

If a set m of outer measures is nonempty, then restricting the infimum of m to s equals the infimum of the restrictions of elements of m to s.

Русский

Если множество внешних мер m непусто, то ограничение инфимума m на s равно инфимууму ограничений элементов m на s.

LaTeX

$$$\operatorname{restrict}_s\bigl(\mathrm{sInf}(m)\bigr) = \mathrm{sInf}\bigl(\operatorname{restrict}_s''m\bigr).$$$

Lean4

/-- This proves that Inf and restrict commute for outer measures, so long as the set of
outer measures is nonempty. -/
theorem restrict_sInf_eq_sInf_restrict (m : Set (OuterMeasure α)) {s : Set α} (hm : m.Nonempty) :
    restrict s (sInf m) = sInf (restrict s '' m) := by simp only [sInf_eq_iInf, restrict_biInf, hm, iInf_image]

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