English
Compact covering of a σ-compact space yields a FiniteSpanningSetsIn structure for a locally finite μ, i.e., a finite spanning sequence of compact sets exists.
Русский
Компактное покрытие σ‑компактного пространства даёт для локально конечной меры μ структуру FiniteSpanningSetsIn, то есть существует конечная последовательность покрывающих компакт-множества.
LaTeX
$$$$\text{If } \alpha \text{ is σ-compact and } μ \text{ locally finite, then } μ\text{ has a finite spanning family of compact sets.}$$$$
Lean4
/-- Compact covering of a `σ`-compact topological space as
`MeasureTheory.Measure.FiniteSpanningSetsIn`. -/
def finiteSpanningSetsInCompact [TopologicalSpace α] [SigmaCompactSpace α] {_ : MeasurableSpace α} (μ : Measure α)
[IsLocallyFiniteMeasure μ] : μ.FiniteSpanningSetsIn {K | IsCompact K}
where
set := compactCovering α
set_mem := isCompact_compactCovering α
finite n := (isCompact_compactCovering α n).measure_lt_top
spanning := iUnion_compactCovering α
