sigmaFinite — Mathlib

English

If μ is sigma-finite, then μ.restrict s is sigma-finite for any s.

Русский

Если μ сигма-конечна, то μ.restrict s сигма-конечна для любого s.

LaTeX

$$instance sigmaFinite (μ : Measure α) [SigmaFinite μ] (s : Set α) : SigmaFinite (μ.restrict s)$$

Lean4

instance sigmaFinite (μ : Measure α) [SigmaFinite μ] (s : Set α) : SigmaFinite (μ.restrict s) :=
  by
  refine ⟨⟨⟨spanningSets μ, fun _ => trivial, fun i => ?_, iUnion_spanningSets μ⟩⟩⟩
  rw [Measure.restrict_apply (measurableSet_spanningSets μ i)]
  exact (measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ i)

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