English
Let α be a topological space and μ a finite Borel measure on α which is inner regular with respect to compact sets; then μ is weakly regular.
Русский
Пусть α — топологическое пространство, μ — конечная борелова мера на α, которая является внутренне регулярной по отношению к компактным множествам; тогда μ обладает свойством слабой регулярности.
LaTeX
$$$[BorelSpace\ α] \land [R1Space\ α] \land [InnerRegularCompactLTTop\ μ] \land [IsFiniteMeasure\ μ] \Rightarrow μ \text{ is WeaklyRegular}$$$
Lean4
instance (priority := 50) [BorelSpace α] [R1Space α] [InnerRegularCompactLTTop μ] [IsFiniteMeasure μ] :
WeaklyRegular μ :=
InnerRegular.innerRegularWRT_isClosed_isOpen.weaklyRegular_of_finite _
