isTightMeasureSet_singleton_of_innerRegular

English

A finite measure that is inner regular with respect to compact sets is tight when considered alone.

Русский

Плотная мера, которая внутренняя регулярна по отношение к компактным множествам, является плотной сама по себе.

LaTeX

$$IsTightMeasureSet { μ }$$

Lean4

/-- Inner regular finite measures on T2 spaces are tight. -/
theorem isTightMeasureSet_singleton_of_innerRegular [T2Space 𝓧] [OpensMeasurableSpace 𝓧] [IsFiniteMeasure μ]
    [h : μ.InnerRegular] : IsTightMeasureSet { μ } :=
  by
  refine isTightMeasureSet_singleton_of_innerRegularWRT ?_
  intro s hs r hr
  obtain ⟨K, hKs, hK_compact, hμK⟩ := h.innerRegular hs r hr
  exact ⟨K, hKs, ⟨hK_compact, hK_compact.isClosed⟩, hμK⟩

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