of_pseudoMetrizableSpace_of_isFiniteMeasure

English

Any finite measure on a pseudo-metrizable space is weakly regular.

Русский

Любая конечная мера на псевдометризируемом пространстве является слаб Reg.

LaTeX

$$$\forall X\text{ pseudo-metrizable space}, μ\text{ finite} \Rightarrow μ \text{ is WeaklyRegular}$$$

Lean4

/-- Any finite measure on a metrizable space (or even a pseudo metrizable space)
is weakly regular. -/
instance (priority := 100) of_pseudoMetrizableSpace_of_isFiniteMeasure {X : Type*} [TopologicalSpace X]
    [PseudoMetrizableSpace X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X) [IsFiniteMeasure μ] :
    WeaklyRegular μ :=
  (InnerRegularWRT.of_pseudoMetrizableSpace μ).weaklyRegular_of_finite μ

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