English
In InnerRegularCompactLTTop with finite measure, for a measurable A with μ(A) ≠ ∞ and a channel r < μ(A), there exists a compact K ⊆ A with μ(A) ≤ μ(K) + (μ(A) − r). As a particular case, for any ε > 0 there exists K ⊆ A with μ(A) < μ(K) + ε.
Русский
При InnerRegularCompactLTTop для A измеримого множества, если μ(A) конечна, и дан r < μ(A), существует компакт K ⊆ A такое, что μ(A) ≤ μ(K) + (μ(A) − r). В частности, для любого ε > 0 найдётся K ⊆ A с μ(A) < μ(K) + ε.
LaTeX
$$$[InnerRegularCompactLTTop μ] \\; ⦃A : Set α⦄, MeasurableSet A → μ A ≠ ∞ → ∀ r < μ A, ∃ K ⊆ A, IsCompact K ∧ μ A < μ K + (μ A − r)$$$
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`. -/
theorem _root_.MeasurableSet.exists_lt_isCompact_of_ne_top [InnerRegularCompactLTTop μ] ⦃A : Set α⦄
(hA : MeasurableSet A) (h'A : μ A ≠ ∞) {r : ℝ≥0∞} (hr : r < μ A) : ∃ K, K ⊆ A ∧ IsCompact K ∧ r < μ K :=
InnerRegularCompactLTTop.innerRegular ⟨hA, h'A⟩ _ hr
