of_pseudoMetrizableSpace_secondCountable_of_locallyFinite

English

Any locally finite measure on a second countable metrizable space (or even pseudo-metrizable) is weakly regular.

Русский

Любая локально конечная мера на пространстве, являющемся вторично счётным метризуемым (или даже псевдо метризуемым), является слабосрегулярной.

LaTeX

$$μ is WeaklyRegular$$

Lean4

/-- Any locally finite measure on a second countable metrizable space
(or even a pseudo metrizable space) is weakly regular. -/
instance (priority := 100) of_pseudoMetrizableSpace_secondCountable_of_locallyFinite {X : Type*} [TopologicalSpace X]
    [PseudoMetrizableSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X)
    [IsLocallyFiniteMeasure μ] : WeaklyRegular μ :=
  have : OuterRegular μ :=
    by
    refine (μ.finiteSpanningSetsInOpen'.mono' fun U hU => ?_).outerRegular
    have : Fact (μ U < ∞) := ⟨hU.2⟩
    exact ⟨hU.1, inferInstance⟩
  ⟨InnerRegularWRT.of_pseudoMetrizableSpace μ⟩

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