English
In a σ-compact space, any closed set can be approximated from inside by a compact subset. For every closed F and every ε > 0 there exists a compact K ⊆ F with μ(F) ≤ μ(K) + ε.
Русский
В σ-замкнутом пространстве каждое замкнутое множество можно аппроксимировать внутри компактным подмножеством: для любого замкнутого F и ε>0 существует K ⊆ F компактное такое, что μ(F) ≤ μ(K) + ε.
LaTeX
$$$\\forall F\\,(IsClosed F)\\;\\forall ε>0:\\; \\exists K\\,(IsCompact K) ∧ K\\subseteq F ∧ μ(F) ≤ μ(K) + ε$$$
Lean4
/-- In a `σ`-compact space, any closed set can be approximated by a compact subset. -/
theorem isCompact_isClosed {X : Type*} [TopologicalSpace X] [SigmaCompactSpace X] [MeasurableSpace X] (μ : Measure X) :
InnerRegularWRT μ IsCompact IsClosed := by
intro F hF r hr
set B : ℕ → Set X := compactCovering X
have hBc : ∀ n, IsCompact (F ∩ B n) := fun n => (isCompact_compactCovering X n).inter_left hF
have hBU : ⋃ n, F ∩ B n = F := by rw [← inter_iUnion, iUnion_compactCovering, Set.inter_univ]
have : μ F = ⨆ n, μ (F ∩ B n) := by
rw [← Monotone.measure_iUnion, hBU]
exact monotone_const.inter monotone_accumulate
rw [this] at hr
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
exact ⟨_, inter_subset_left, hBc n, hn⟩
