English
A variant of the same outer-approximation property for compact sets under inner regularity assumptions.
Русский
Вариант той же внешней аппроксимации для компактных множеств при предположениях внутренней регулярности.
LaTeX
$$$\forall K\text{ компакт},\ \forall ε>0:\exists U\supset K,\ IsOpen(U)\land μ(U) < μ(K) + ε$$$
Lean4
/-- Let `μ` be a locally finite measure on an R₁ topological space with Borel σ-algebra.
If `μ` is inner regular for finite measure sets with respect to compact sets,
then any null measurable set of finite measure can be approximated in measure by an open set.
See also `Set.exists_isOpen_lt_of_lt` and `MeasurableSet.exists_isOpen_diff_lt`
for the case of an outer regular measure. -/
protected theorem _root_.MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt [InnerRegularCompactLTTop μ]
[IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α} (hs : NullMeasurableSet s μ) (hμs : μ s ≠ ∞)
{ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ U, IsOpen U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε :=
by
rcases hs with ⟨t, htm, hst⟩
rcases htm.exists_isOpen_symmDiff_lt (by rwa [← measure_congr hst]) hε with ⟨U, hUo, hμU, hUs⟩
refine ⟨U, hUo, hμU, ?_⟩
rwa [measure_congr <| (ae_eq_refl _).symmDiff hst]
