innerRegular_isCompact_isClosed_measurableSet

English

On Polish spaces, a finite measure is inner regular with respect to compact and closed sets, providing regularity for finite measures on such spaces.

Русский

На полис пространствах конечная мера обладает внутренней регулярностью по компактно-замкнутым множествам, обеспечивая регулярность для конечных мер на таких пространствах.

LaTeX

$$$\forall A \in \mathcal{M}(\alpha),\; μ(A) = \sup\{ μ(K) : K \subseteq A,\ K \text{ compact and closed} \}.$$$

Lean4

/-- On a Polish space, any finite measure is regular with respect to compact and closed sets. In
particular, a finite measure on a Polish space is a tight measure.
-/
theorem innerRegular_isCompact_isClosed_measurableSet [TopologicalSpace α] [PolishSpace α] [BorelSpace α]
    (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet :=
  by
  letI := TopologicalSpace.upgradeIsCompletelyMetrizable α
  exact innerRegular_isCompact_isClosed_measurableSet_of_finite P

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