instRegularOfBorelSpaceOfR1SpaceOfIsFiniteMeasure

English

If μ is inner regular for compact LTTop sets and μ is finite, then μ is a regular measure.

Русский

Если μ является внутренне регулярной по отношению к компактным множествам с LTTop и μ конечна, то μ является регулярной мерой.

LaTeX

$$$[BorelSpace\ α] \land [R1Space\ α] \land [h : InnerRegularCompactLTTop\ μ] \land [IsFiniteMeasure\ μ] \Rightarrow μ \text{ is Regular}$$$

Lean4

instance (priority := 50) [BorelSpace α] [R1Space α] [h : InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] : Regular μ
    where
  innerRegular :=
    InnerRegularWRT.trans h.innerRegular <| InnerRegularWRT.of_imp (fun U hU ↦ ⟨hU.measurableSet, measure_ne_top μ U⟩)

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