English
Let μ be a measure on a space with a suitable pseudo-metric structure that is complete and second-countable, and has a Borel σ-algebra. Then μ is inner regular with respect to compact sets for finite-measure sets: for any measurable A with μ(A) < ∞, one has μ(A) = sup { μ(K) : K ⊆ A, K compact }.
Русский
Пусть μ — мера на пространстве с подходящим псевдометрическим строением, которое полно и счётно, и имеет борелеву σ-алгебру. Тогда μ внутри регулярно относительно компактных множеств для множеств с конечной мерой: для любого измеримого A с μ(A) < ∞ выполняется μ(A) = sup { μ(K) : K ⊆ A, K компакт }.
LaTeX
$$$\forall A \in \mathcal{M}(\alpha),\; μ(A) = \sup\{ μ(K) : K \subseteq A,\ K \text{ compact} \}.$$$
Lean4
/-- A measure `μ` on a `PseudoEMetricSpace E` and `CompleteSpace E` with `SecondCountableTopology E`
is inner regular for finite measure sets with respect to compact sets.
-/
instance InnerRegularCompactLTTop_of_pseudoEMetricSpace_completeSpace_secondCountable [PseudoEMetricSpace α]
[CompleteSpace α] [SecondCountableTopology α] [BorelSpace α] (μ : Measure α) : μ.InnerRegularCompactLTTop :=
by
constructor
intro A ⟨hA1, hA2⟩ r hr
have := Fact.mk hA2.lt_top
have hA2' : (μ.restrict A) A ≠ ⊤ := by rwa [Measure.restrict_apply_self]
have hr' : r < μ.restrict A A := by rwa [Measure.restrict_apply_self]
obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ := MeasurableSet.exists_lt_isCompact_of_ne_top hA1 hA2' hr'
use K, hK1, hK2
rwa [Measure.restrict_eq_self μ hK1] at hK3
