English
A content μ is regular if for every compact K, μ(K) equals the infimum of μ(K') over all K' containing K with K ⊂ int K' ⊂ K'.
Русский
Контент μ называется регулярным, если для каждого компактного K: μ(K) = inf { μ(K') : K ⊆ interior(K') }.
LaTeX
$$$$\\text{ContentRegular: } μ K = \\inf_{K'\\ } μ K' \\quad (K' \\text{ compact}, K \\subseteq \\operatorname{int}K').$$$$
Lean4
/-- In a locally compact space, any measure constructed from a content is regular. -/
instance regular [WeaklyLocallyCompactSpace G] : μ.measure.Regular :=
by
have : IsFiniteMeasureOnCompacts μ.measure := by
refine ⟨fun K hK => ?_⟩
apply (measure_mono subset_closure).trans_lt _
rw [measure_apply _ isClosed_closure.measurableSet]
exact μ.outerMeasure_lt_top_of_isCompact hK.closure
refine ⟨fun U hU r hr => ?_⟩
rw [measure_apply _ hU.measurableSet, μ.outerMeasure_of_isOpen U hU] at hr
simp only [innerContent, lt_iSup_iff] at hr
rcases hr with ⟨K, hKU, hr⟩
refine ⟨K, hKU, K.2, hr.trans_le ?_⟩
exact (μ.le_outerMeasure_compacts K).trans (le_toMeasure_apply _ _ _)
