English
A locally finite measure on a σ-compact space admits a finite spanning sequence of open sets.
Русский
Локально конечная мера на σ-компактном пространстве допускает конечную последовательность открытых покрытий, образующих spanning.
LaTeX
$$$$\text{There exists a finite spanning sequence of open sets }\{U_n\} \text{ with } U_n \text{ open and } \bigcup_n U_n = X.$$$$
Lean4
/-- A locally finite measure on a `σ`-compact topological space admits a finite spanning sequence
of open sets. -/
def finiteSpanningSetsInOpen [TopologicalSpace α] [SigmaCompactSpace α] {_ : MeasurableSpace α} (μ : Measure α)
[IsLocallyFiniteMeasure μ] : μ.FiniteSpanningSetsIn {K | IsOpen K}
where
set n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose
set_mem n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.1
finite n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.2
spanning :=
eq_univ_of_subset
(iUnion_mono fun n => ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.1)
(iUnion_compactCovering α)
