English
If InnerRegularCompactLTTop μ holds, then any measurable set of finite measure can be approximated from inside by a compact subset: there exists K ⊆ A with K compact and μ(A) < μ(K) + ε.
Русский
При InnerRegularCompactLTTop μ любое измеримое множество с конечной мерой можно аппроксимировать внутри компактным подмножеством: существует K ⊆ A с K компактно и μ(A) < μ(K) + ε.
LaTeX
$$$[InnerRegularCompactLTTop μ] [OpensMeasurableSpace α]\\; (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_lt_isCompact_of_ne_top`. -/
theorem _root_.MeasurableSet.exists_isCompact_lt_add [InnerRegularCompactLTTop μ] ⦃A : Set α⦄ (hA : MeasurableSet A)
(h'A : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) : ∃ K, K ⊆ A ∧ IsCompact K ∧ μ A < μ K + ε :=
InnerRegularCompactLTTop.innerRegular.exists_subset_lt_add isCompact_empty ⟨hA, h'A⟩ h'A hε
