English
Let α be a type with a measurable structure such that the space supports a complete metric-like structure and second-countable topology, and μ be a finite measure on α. Then μ is inner regular (tight); that is, for every measurable set A, μ(A) = sup { μ(K) : K ⊆ A, K compact }.
Русский
Пусть α — множество с мерею и метрическим образом пространства, обладающее полнотой и второй счётностью, и μ — конечная мера на α. Тогда μ является внутренне регулярной (tight); то есть для любого измеримого множества A выполняется μ(A) = sup { μ(K) : K ⊆ A, K компактно }.
LaTeX
$$$\forall A \in \mathcal{M}(\alpha):\quad \mu(A) = \sup\{ \mu(K) : K \subseteq A,\ K \text{ compact} \}.$$$
Lean4
/-- A finite measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with
`SecondCountableTopology E` is inner regular. In other words, a finite measure
on such a space is a tight measure.
-/
instance InnerRegular_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α] [CompleteSpace α]
[SecondCountableTopology α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegular :=
by
suffices P.InnerRegularCompactLTTop from inferInstance
refine ⟨Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_⟩
· exact innerRegularWRT_isCompact_isOpen P
· exact fun s t hs_compact ht_open ↦ hs_compact.inter_right ht_open.isClosed_compl
