Exhaustions of analytic K-spaces

An analytic K-space is countable at infinity [Hir64, Ch. 0, §1, p. 120, clause (ii)] — a countable increasing union of relatively compact open subspaces, as Hir64, Ch. 0, §1, p. 121, footnote 10 words it for real spaces — and the resolution of [Kol07, 44] is obtained on such a space from resolutions of neighbourhoods of compact sets; the gluing of [Wlo09, §4] and [Wlo09, §4.3] likewise starts from an open cover with compact closures.

• exists_opens_isCompact_closure_superset: in a weakly locally compact Hausdorff space a compact set lies in an open set with compact closure (the interior of Mathlib's exists_compact_superset).
• AnalyticSpace.exists_exhaustion: an analytic K-space is exhausted by relatively compact opens U₀ ⋐ U₁ ⋐ ⋯ with ⋃ Uₙ = X — the opens relCompactOpen of Hironaka/Manifold/Exhaustion.lean cut out of Mathlib's CompactExhaustion.choice, which exists because the space is locally compact, σ-compact and Hausdorff.

Used by Hironaka/Resolution/Analytic/Kol07Thm45/PieceGlueIndep.lean and Hironaka/Resolution/Analytic/Kol07Thm45/PieceGlueProof.lean.

theorem AnalyticSpace.exists_opens_isCompact_closure_superset {M : Type u_1} [TopologicalSpace M] [WeaklyLocallyCompactSpace M] [T2Space M] {S : Set M} (hS : IsCompact S) : ∃ (W : TopologicalSpace.Opens M), S ⊆ ↑W ∧ IsCompact (closure ↑W)

In a weakly locally compact Hausdorff space, a compact set lies in an open set with compact closure (compare the opens Vᵢ ⊆ Wᵢ with compact closures of [Wlo09, §4]): the interior of a compact neighbourhood K' (exists_compact_superset), whose closure is a closed subset of K'.

theorem AnalyticSpace.exists_exhaustion {K : Type} [RCLike K] (X : AnalyticSpace K) : ∃ (U : ℕ → TopologicalSpace.Opens ↑↑X.toPresheafedSpace), (∀ (n : ℕ), IsCompact (closure ↑(U n))) ∧ (∀ (n : ℕ), closure ↑(U n) ⊆ ↑(U (n + 1))) ∧ ⋃ (n : ℕ), ↑(U n) = Set.univ

An analytic K-space is exhausted by relatively compact opens U₀ ⋐ U₁ ⋐ ⋯ with ⋃ Uₙ = X ([Kol07, 44]; [Hir64, Ch. 0, §1, p. 120, clause (ii)]): the opens relCompactOpen of Hironaka/Manifold/Exhaustion.lean cut out of Mathlib's CompactExhaustion.choice X, which exists by local compactness and σ-compactness.