English
For a measurable set A of finite μ-measure in a suitable regularity setting, there exists a compact closed K ⊆ A such that μ(A) < μ(K) + ε for any ε > 0.
Русский
Для измеримого множества A с конечной мерой существует компактное замкнутое K ⊆ A такое, что μ(A) < μ(K) + ε для любого ε > 0.
LaTeX
$$$[InnerRegularCompactLTTop μ] [R1Space α] [BorelSpace α]\\; (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε > 0}:\\; ∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε$$$
Lean4
/-- If `μ` is inner regular, then any measurable set can be approximated by a compact subset.
See also `MeasurableSet.exists_isCompact_lt_add_of_ne_top`. -/
theorem _root_.MeasurableSet.exists_lt_isCompact [InnerRegular μ] ⦃A : Set α⦄ (hA : MeasurableSet A) {r : ℝ≥0∞}
(hr : r < μ A) : ∃ K, K ⊆ A ∧ IsCompact K ∧ r < μ K :=
InnerRegular.innerRegular hA _ hr
