English
On a Polish space, any finite measure is inner regular. Specifically, if α is a Polish space with its Borel measurable structure and μ is a finite measure on α, then μ is inner regular.
Русский
На полищ пространства любая конечная мера является внутренне регулярной. Пусть α — полиш-пространство с борелевой σ-алгеброй и μ — конечная мера на α; тогда μ является внутренне регулярной.
LaTeX
$$$\forall A \in \mathcal{M}(\alpha):\quad \mu(A) = \sup\{ \mu(K) : K \subseteq A,\ K \text{ compact} \}. $$$
Lean4
/-- A special case of `innerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable` for Polish
spaces: A finite measure on a Polish space is a tight measure.
-/
instance InnerRegular_of_polishSpace [TopologicalSpace α] [PolishSpace α] [BorelSpace α] (P : Measure α)
[IsFiniteMeasure P] : P.InnerRegular :=
by
letI := TopologicalSpace.upgradeIsCompletelyMetrizable α
exact InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable P
