English
In inner regular compact LTTop setting with R1 spaces, for any measurable A with finite μ(A) there exists a compact K ⊆ A with μ A < μ K + ε, and K is closed.
Русский
В условиях внутренней регулярности для компактных множеств и R1-пространства для измеримого A конечной меры существует компактное K ⊆ A с μ(A) < μ(K) + ε и K замкнуто.
LaTeX
$$$[InnerRegularCompactLTTop μ][R1Space α][BorelSpace α]\\; (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) : \\exists K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε$$$
Lean4
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a compact closed subset.
Compared to `MeasurableSet.exists_isCompact_lt_add`,
this version additionally assumes that `α` is an R₁ space with Borel σ-algebra.
-/
theorem _root_.MeasurableSet.exists_isCompact_isClosed_lt_add [InnerRegularCompactLTTop μ] [R1Space α] [BorelSpace α]
⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε :=
let ⟨K, hKA, hK, hμK⟩ := hA.exists_isCompact_lt_add h'A hε
⟨closure K, hK.closure_subset_measurableSet hA hKA, hK.closure, isClosed_closure, by rwa [hK.measure_closure]⟩
