English
Same as above: there exists an open U containing a compact K with μ(U) arbitrarily close to μ(K) from above.
Русский
Аналогично: существует открытое U, содержащее K, такое что μ(U) может быть произвольно близко к μ(K) сверху.
LaTeX
$$$\forall ε>0,\ ∃ U\ (K\subset U)\land 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 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_.MeasurableSet.exists_isOpen_symmDiff_lt [InnerRegularCompactLTTop μ] [IsLocallyFiniteMeasure μ]
[R1Space α] [BorelSpace α] {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ U, IsOpen U ∧ μ U < ∞ ∧ μ (U ∆ s) < ε :=
by
have : ε / 2 ≠ 0 := (ENNReal.half_pos hε).ne'
rcases hs.exists_isCompact_isClosed_diff_lt hμs this with ⟨K, hKs, hKco, hKcl, hμK⟩
rcases hKco.exists_isOpen_lt_add (μ := μ) this with ⟨U, hKU, hUo, hμU⟩
refine ⟨U, hUo, hμU.trans_le le_top, ?_⟩
rw [← ENNReal.add_halves ε, measure_symmDiff_eq hUo.nullMeasurableSet hs.nullMeasurableSet]
gcongr
·
calc
μ (U \ s) ≤ μ (U \ K) := by gcongr
_ < ε / 2 := by
apply measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKU _ hμU
exact ne_top_of_le_ne_top hμs (by gcongr)
· exact lt_of_le_of_lt (by gcongr) hμK
