English
If μ is inner regular for finite-measure sets with respect to compact sets, then for a measurable A with μ(A) ≠ ∞ there exists a compact K ⊆ A with μ(A) < μ(K) + ε, i.e., A can be approximated from inside by a compact subset with small deficit.
Русский
Если μ — внутренняя регуляность для конечномерных множеств по отношению к компакт-множесткам, то для измеримого A с μ(A) ≠ ∞ существует K ⊆ A компактное, такое что μ(A) < μ(K) + ε.
LaTeX
$$$[OpensMeasurableSpace α][T2Space α][InnerRegularCompactLTTop μ]\\; (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε ≠ 0}: \\exists K, K ⊆ A ∧ IsCompact 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 subset. See also `MeasurableSet.exists_isCompact_lt_add` and
`MeasurableSet.exists_lt_isCompact_of_ne_top`. -/
theorem _root_.MeasurableSet.exists_isCompact_diff_lt [OpensMeasurableSpace α] [T2Space α] [InnerRegularCompactLTTop μ]
⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ K, K ⊆ A ∧ IsCompact K ∧ μ (A \ K) < ε :=
by
rcases hA.exists_isCompact_lt_add h'A hε with ⟨K, hKA, hKc, hK⟩
exact
⟨K, hKA, hKc, measure_diff_lt_of_lt_add hKc.nullMeasurableSet hKA (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩
