iSup_restrict_spanningSets — Mathlib

English

In a σ-finite space, for any set s, the supremum over i of μ.restrict (spanningSets μ i) applied to s equals μ s.

Русский

В пространства с сигма‑конечной мерой, для любого множества s, суммарно над i выполняется равенство μ.restrict (spanningSets μ i) (s) = μ(s).

LaTeX

$$$[SigmaFinite μ] (s : Set α) : ⨆ i, μ.restrict (spanningSets μ i) s = μ s$$$

Lean4

theorem iSup_restrict_spanningSets [SigmaFinite μ] (s : Set α) : ⨆ i, μ.restrict (spanningSets μ i) s = μ s :=
  by
  rw [← measure_toMeasurable s, ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]
  simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s, ←
    restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]

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