English
For A measurable with finite μ(A) in the InnerRegularCompactLTTop setting, there exists a K ⊆ A that is compact and closed such that μ(A) < μ(K) + ε.
Русский
Для измеримого A с конечной μ(A) в условиях InnerRegularCompactLTTop существует K ⊆ A, который компактный и замкнутый, такой что μ(A) < μ(K) + ε.
LaTeX
$$$[BorelSpace α][R1Space α][InnerRegularCompactLTTop μ]\\; ⦃A : Set α⦄, (hA : MeasurableSet A) (h'A : μ A ≠ ∞) {ε : ENNReal} (hε : ε ≠ 0) : ∃ K, K ⊆ A ∧ IsCompact K ∧ IsClosed K ∧ μ A < μ K + ε$$$
Lean4
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
any measurable set of finite mass can be approximated from inside by compact sets. -/
theorem _root_.MeasurableSet.measure_eq_iSup_isCompact_of_ne_top [InnerRegularCompactLTTop μ] ⦃A : Set α⦄
(hA : MeasurableSet A) (h'A : μ A ≠ ∞) : μ A = ⨆ (K) (_ : K ⊆ A) (_ : IsCompact K), μ K :=
InnerRegularCompactLTTop.innerRegular.measure_eq_iSup ⟨hA, h'A⟩
