English
A regular measure is regular with respect to compact closures: inner-regularity via closure is equivalent to standard inner-regularity.
Русский
Регулярная мера эквивалентна регулярности по компактным замыканиям: внутренняя регулярность через замыкание равна обычной внутренней регулярности.
LaTeX
$$$\\text{Regular}(\\mu) \\iff \\text{InnerRegularWRTIsCompactClosure}(\\mu).$$$
Lean4
/-- Any sigma finite measure on a `σ`-compact pseudometrizable space is inner regular. -/
instance (priority := 100) {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X] [SigmaCompactSpace X]
[MeasurableSpace X] [BorelSpace X] (μ : Measure X) [SigmaFinite μ] : InnerRegular μ :=
by
refine ⟨(InnerRegularWRT.isCompact_isClosed μ).trans ?_⟩
refine InnerRegularWRT.of_restrict (fun n ↦ ?_) (iUnion_spanningSets μ).superset (monotone_spanningSets μ)
have : Fact (μ (spanningSets μ n) < ∞) := ⟨measure_spanningSets_lt_top μ n⟩
exact WeaklyRegular.innerRegular_measurable.trans InnerRegularWRT.of_sigmaFinite
