iSup_restrict_spanningSets_of_measurableSet

English

For a σ-finite μ, and a measurable set s, the supremum over i of μ.restrict (spanningSets μ i) applied to s equals μ s.

Русский

Для σ‑конечной μ и измеримого множества s супремум по i от μ.restrict(spanningSets μ i) применённому к s равен μ s.

LaTeX

$$$[SigmaFinite μ] (hs : MeasurableSet s) : \; ⨆ i, μ.restrict (spanningSets μ i) s = μ s$$$

Lean4

/-- Auxiliary lemma for `iSup_restrict_spanningSets`. -/
theorem iSup_restrict_spanningSets_of_measurableSet [SigmaFinite μ] (hs : MeasurableSet s) :
    ⨆ i, μ.restrict (spanningSets μ i) s = μ s :=
  calc
    ⨆ i, μ.restrict (spanningSets μ i) s = μ.restrict (⋃ i, spanningSets μ i) s :=
      (restrict_iUnion_apply_eq_iSup (monotone_spanningSets μ).directed_le hs).symm
    _ = μ s := by rw [iUnion_spanningSets, restrict_univ]

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