English
Let μ be a measure on a topological space, inner regular with respect to a predicate p on open sets. If s is measurable with μ(s) finite, then for every ε > 0 there exists a subset K ⊆ s such that p(K) holds and μ(s \\ K) < ε. (In particular, s can be approximated from inside by sets satisfying p.)
Русский
Пусть μ — мера на топологическом пространстве, являющаяся внутренне регулярной по предикату p на открытые множества. Если s измерима и μ(s) ограничена, то для любого ε > 0 существует подмножество K ⊆ s такое, что p(K) выполняется и μ(s \\ K) < ε. (В частности, s можно аппроксимировать изнутри множествами, удовлетворяющими p.)
LaTeX
$$$\\forall s\\,(MeasurableSet\\,s \\land μ\\,s \\neq ∞)\\;\\forall ε>0:\\;\\exists K\\subseteq s:\\; p\\,K \\land μ\\,(s\\setminus K) < ε$$$
Lean4
/-- If a measure is inner regular (using closed or compact sets) for open sets, then every
measurable set of finite measure can be approximated by a (closed or compact) subset. -/
theorem measurableSet_of_isOpen [OuterRegular μ] (H : InnerRegularWRT μ p IsOpen)
(hd : ∀ ⦃s U⦄, p s → IsOpen U → p (s \ U)) : InnerRegularWRT μ p fun s => MeasurableSet s ∧ μ s ≠ ∞ :=
by
rintro s ⟨hs, hμs⟩ r hr
have h0 : p ∅ := by
have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
simpa using hd hK isOpen_univ
obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) :=
by
use (μ s - r) / 2
simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, tsub_eq_zero_iff_le]
rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩
rcases (U \ s).exists_isOpen_lt_of_lt _ hμU with ⟨U', hsU', hU'o, hμU'⟩
replace hsU' := diff_subset_comm.1 hsU'
rcases H.exists_subset_lt_add h0 hUo hUt.ne hε with ⟨K, hKU, hKc, hKr⟩
refine ⟨K \ U', fun x hx => hsU' ⟨hKU hx.1, hx.2⟩, hd hKc hU'o, ENNReal.sub_lt_of_lt_add hεs ?_⟩
calc
μ s ≤ μ U := μ.mono hsU
_ < μ K + ε := hKr
_ ≤ μ (K \ U') + μ U' + ε := (add_le_add_right (tsub_le_iff_right.1 le_measure_diff) _)
_ ≤ μ (K \ U') + ε + ε := by gcongr
_ = μ (K \ U') + (ε + ε) := add_assoc _ _ _
