English
Under similar hypotheses, there exists a compact K ⊆ A such that K is closed and μ(A \\ K) < ε.
Русский
При аналогичных предположениях существует компактное K ⊆ A, которое замкнуто и μ(A \\ K) < ε.
LaTeX
$$$[InnerRegularCompactLTTop μ][BorelSpace α][R1Space α]\\; (hA : MeasurableSet A)(h'A : μ A ≠ ∞){ε ≠ 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_diff_lt`,
this lemma additionally assumes that `α` is an R₁ space with Borel σ-algebra. -/
theorem _root_.MeasurableSet.exists_isCompact_isClosed_diff_lt [BorelSpace α] [R1Space α] [InnerRegularCompactLTTop μ]
⦃A : Set α⦄ (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ (A \ K) < ε :=
by
rcases hA.exists_isCompact_isClosed_lt_add h'A hε with ⟨K, hKA, hKco, hKcl, hK⟩
exact
⟨K, hKA, hKco, hKcl,
measure_diff_lt_of_lt_add hKcl.nullMeasurableSet hKA (ne_top_of_le_ne_top h'A <| measure_mono hKA) hK⟩
