English
For finite measures on a pseudo-metric complete second-countable space, one has inner regularity with respect to sets that are compact and closed, i.e., for any measurable A, μ(A) equals the supremum of μ(K) over K ⊆ A with K compact and closed.
Русский
Для конечных мер на псевдометрическом полном пространстве счётности имеется внутренняя регулярность относительно множеств, которые компактны и замкнуты: для любого измеримого A выполняется μ(A) = sup{ μ(K) : K ⊆ A, K компактно и замкнуто }.
LaTeX
$$$\forall A \in \mathcal{M}(\alpha),\; μ(A) = \sup\{ μ(K) : K \subseteq A,\ K \text{ compact and closed} \}.$$$
Lean4
theorem innerRegular_isCompact_isClosed_measurableSet_of_finite [PseudoEMetricSpace α] [CompleteSpace α]
[SecondCountableTopology α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet :=
by
suffices P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) fun s ↦ MeasurableSet s ∧ P s ≠ ∞
by
convert this
simp only [iff_self_and]
exact fun _ ↦ measure_ne_top P _
refine Measure.InnerRegularWRT.measurableSet_of_isOpen ?_ ?_
· exact innerRegularWRT_isCompact_isClosed_isOpen P
· rintro s t ⟨hs_compact, hs_closed⟩ ht_open
rw [diff_eq]
exact ⟨hs_compact.inter_right ht_open.isClosed_compl, hs_closed.inter (isClosed_compl_iff.mpr ht_open)⟩
