of_sigmaCompactSpace_of_isLocallyFiniteMeasure

English

For a finite-measure regular P, and any ε>0, there exists a compact closure K with P(K^c) < ε.

Русский

Для конечномерной меры P и любого ε>0 существует компактное замыкание K такое, что P(K^c) < ε.

LaTeX

$$$\\exists K, \\operatorname{IsCompact}(\\overline{K}) \\wedge P(K^{c}) < \\varepsilon.$$$

Lean4

/-- Any locally finite measure on a `σ`-compact pseudometrizable space is regular. -/
instance (priority := 100) of_sigmaCompactSpace_of_isLocallyFiniteMeasure {X : Type*} [TopologicalSpace X]
    [PseudoMetrizableSpace X] [SigmaCompactSpace X] [MeasurableSpace X] [BorelSpace X] (μ : Measure X)
    [IsLocallyFiniteMeasure μ] : Regular μ :=
  by
  let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  exact ⟨(InnerRegularWRT.isCompact_isClosed μ).trans (InnerRegularWRT.of_pseudoMetrizableSpace μ)⟩

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