toFiniteSpanningSetsIn — Mathlib

English

For a σ-finite μ, toFiniteSpanningSetsIn μ assigns to each n a finite-measure set that spans the universe.

Русский

Для σ-конечной μ toFiniteSpanningSetsIn μ сопоставляет для каждого n множество с конечной мерой, которое охватывает вселенную.

LaTeX

$$toFiniteSpanningSetsIn (μ) : μ.FiniteSpanningSetsIn {s | MeasurableSet s}$$

Lean4

/-- If `μ` is σ-finite it has finite spanning sets in the collection of all measurable sets. -/
def toFiniteSpanningSetsIn (μ : Measure α) [h : SigmaFinite μ] : μ.FiniteSpanningSetsIn {s | MeasurableSet s}
    where
  set n := toMeasurable μ (h.out.some.set n)
  set_mem _ := measurableSet_toMeasurable _ _
  finite
    n := by
    rw [measure_toMeasurable]
    exact h.out.some.finite n
  spanning := eq_univ_of_subset (iUnion_mono fun _ => subset_toMeasurable _ _) h.out.some.spanning

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