English
A choice of an exhaustion by compact sets for a weakly locally compact σ-compact space exists: there is a function that assigns to each natural number a compact subset in a nested, exhaustive manner.
Русский
Существование выбора исчерпывания пространств компактными множествами для слабократно локально компактного σ-компактного пространства: существует функция, которая каждому натуральному числу сопоставляет компактное множество, образующее вложенное исчерпывание.
LaTeX
$$$$\text{choice}: (X) \, [TopologicalSpace X] \, [WeaklyLocallyCompactSpace X] \, [SigmaCompactSpace X] \to CompactExhaustion X.$$$$
Lean4
/-- A choice of an
[exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets)
of a weakly locally compact σ-compact space. -/
noncomputable def choice (X : Type*) [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] :
CompactExhaustion X := by
apply Classical.choice
let K : ℕ → { s : Set X // IsCompact s } := fun n =>
Nat.recOn n ⟨∅, isCompact_empty⟩ fun n s =>
⟨(exists_compact_superset s.2).choose ∪ compactCovering X n,
(exists_compact_superset s.2).choose_spec.1.union (isCompact_compactCovering _ _)⟩
refine ⟨⟨fun n ↦ (K n).1, fun n => (K n).2, fun n ↦ ?_, ?_⟩⟩
· exact Subset.trans (exists_compact_superset (K n).2).choose_spec.2 (interior_mono subset_union_left)
· refine univ_subset_iff.1 (iUnion_compactCovering X ▸ ?_)
exact iUnion_mono' fun n => ⟨n + 1, subset_union_right⟩
