doc-next-gen

Mathlib.Topology.Compactness.SigmaCompact

Module docstring

{"# Sigma-compactness in topological spaces

Main definitions

  • IsSigmaCompact: a set that is the union of countably many compact sets.
  • SigmaCompactSpace X: X is a σ-compact topological space; i.e., is the union of a countable collection of compact subspaces.

"}

IsSigmaCompact definition
(s : Set X) : Prop
Full source 
/-- A subset `s ⊆ X` is called **σ-compact** if it is the union of countably many compact sets. -/
def IsSigmaCompact (s : Set X) : Prop :=
  ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = s
$\sigma$-compact subset
Informal description
A subset $s$ of a topological space $X$ is called $\sigma$-compact if there exists a countable family of compact subsets $K_n \subseteq X$ such that $s = \bigcup_{n} K_n$.
isSigmaCompact_iUnion_of_isCompact theorem
[hι : Countable ι] (s : ι → Set X) (hcomp : ∀ i, IsCompact (s i)) : IsSigmaCompact (⋃ i, s i)
Full source 
/-- Countable unions of compact sets are σ-compact. -/
lemma isSigmaCompact_iUnion_of_isCompact [hι : Countable ι] (s : ι → Set X)
    (hcomp : ∀ i, IsCompact (s i)) : IsSigmaCompact (⋃ i, s i) := by
  rcases isEmpty_or_nonempty ι
  · simp only [iUnion_of_empty, isSigmaCompact_empty]
  · -- If ι is non-empty, choose a surjection f : ℕ → ι, this yields a map ℕ → Set X.
    obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι
    exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩
Countable Union of Compact Sets is $\sigma$-Compact
Informal description
Let $X$ be a topological space and $\{s_i\}_{i \in \iota}$ be a countable family of subsets of $X$ (where $\iota$ is a countable index set). If each $s_i$ is compact, then their union $\bigcup_{i \in \iota} s_i$ is $\sigma$-compact.
isSigmaCompact_sUnion_of_isCompact theorem
{S : Set (Set X)} (hc : Set.Countable S) (hcomp : ∀ (s : Set X), s ∈ S → IsCompact s) : IsSigmaCompact (⋃₀ S)
Full source 
/-- Countable unions of compact sets are σ-compact. -/
lemma isSigmaCompact_sUnion_of_isCompact {S : Set (Set X)} (hc : Set.Countable S)
    (hcomp : ∀ (s : Set X), s ∈ S → IsCompact s) : IsSigmaCompact (⋃₀ S) := by
  have : Countable S := countable_coe_iff.mpr hc
  rw [sUnion_eq_iUnion]
  apply isSigmaCompact_iUnion_of_isCompact _ (fun ⟨s, hs⟩ ↦ hcomp s hs)
Countable Union of Compact Sets is $\sigma$-Compact
Informal description
Let $X$ be a topological space and $S$ be a countable collection of subsets of $X$. If every set $s \in S$ is compact, then the union $\bigcup S$ is $\sigma$-compact.
isSigmaCompact_iUnion theorem
[Countable ι] (s : ι → Set X) (hcomp : ∀ i, IsSigmaCompact (s i)) : IsSigmaCompact (⋃ i, s i)
Full source 
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_iUnion [Countable ι] (s : ι → Set X)
    (hcomp : ∀ i, IsSigmaCompact (s i)) : IsSigmaCompact (⋃ i, s i) := by
  -- Choose a decomposition s_i = ⋃ K_i,j for each i.
  choose K hcomp hcov using fun i ↦ hcomp i
  -- Then, we have a countable union of countable unions of compact sets, i.e. countably many.
  have := calc
    ⋃ i, s i
    _ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
    _ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
    _ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']
  rw [this]
  exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)
Countable Union of $\sigma$-Compact Sets is $\sigma$-Compact
Informal description
Let $X$ be a topological space and $\{s_i\}_{i \in \iota}$ be a countable family of subsets of $X$ (where $\iota$ is a countable index set). If each $s_i$ is $\sigma$-compact, then their union $\bigcup_{i \in \iota} s_i$ is also $\sigma$-compact.
isSigmaCompact_sUnion theorem
(S : Set (Set X)) (hc : Set.Countable S) (hcomp : ∀ s : S, IsSigmaCompact s (X := X)) : IsSigmaCompact (⋃₀ S)
Full source 
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_sUnion (S : Set (Set X)) (hc : Set.Countable S)
    (hcomp : ∀ s : S, IsSigmaCompact s (X := X)) : IsSigmaCompact (⋃₀ S) := by
  have : Countable S := countable_coe_iff.mpr hc
  apply sUnion_eq_iUnion.symm ▸ isSigmaCompact_iUnion _ hcomp
Countable Union of $\sigma$-Compact Sets is $\sigma$-Compact
Informal description
Let $X$ be a topological space and $S$ be a countable collection of subsets of $X$. If every set $s \in S$ is $\sigma$-compact, then the union $\bigcup S$ is $\sigma$-compact.
isSigmaCompact_biUnion theorem
{s : Set ι} {S : ι → Set X} (hc : Set.Countable s) (hcomp : ∀ (i : ι), i ∈ s → IsSigmaCompact (S i)) : IsSigmaCompact (⋃ (i : ι) (_ : i ∈ s), S i)
Full source 
/-- Countable unions of σ-compact sets are σ-compact. -/
lemma isSigmaCompact_biUnion {s : Set ι} {S : ι → Set X} (hc : Set.Countable s)
    (hcomp : ∀ (i : ι), i ∈ s → IsSigmaCompact (S i)) :
    IsSigmaCompact (⋃ (i : ι) (_ : i ∈ s), S i) := by
  have : Countable ↑s := countable_coe_iff.mpr hc
  rw [biUnion_eq_iUnion]
  exact isSigmaCompact_iUnion _ (fun ⟨i', hi'⟩ ↦ hcomp i' hi')
Countable Union of $\sigma$-Compact Sets is $\sigma$-Compact
Informal description
Let $X$ be a topological space, $\iota$ an index set, and $s \subseteq \iota$ a countable subset. For each $i \in s$, let $S_i \subseteq X$ be a $\sigma$-compact subset. Then the union $\bigcup_{i \in s} S_i$ is $\sigma$-compact.
IsSigmaCompact.of_isClosed_subset theorem
{s t : Set X} (ht : IsSigmaCompact t) (hs : IsClosed s) (h : s ⊆ t) : IsSigmaCompact s
Full source 
/-- A closed subset of a σ-compact set is σ-compact. -/
lemma IsSigmaCompact.of_isClosed_subset {s t : Set X} (ht : IsSigmaCompact t)
    (hs : IsClosed s) (h : s ⊆ t) : IsSigmaCompact s := by
  rcases ht with ⟨K, hcompact, hcov⟩
  refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩
  rw [← inter_iUnion, hcov]
  exact inter_eq_left.mpr h
Closed Subset of $\sigma$-Compact Set is $\sigma$-Compact
Informal description
Let $X$ be a topological space, and let $s, t \subseteq X$ be subsets such that $t$ is $\sigma$-compact and $s$ is a closed subset of $t$. Then $s$ is $\sigma$-compact.
IsSigmaCompact.image_of_continuousOn theorem
{f : X → Y} {s : Set X} (hs : IsSigmaCompact s) (hf : ContinuousOn f s) : IsSigmaCompact (f '' s)
Full source 
/-- If `s` is σ-compact and `f` is continuous on `s`, `f(s)` is σ-compact. -/
lemma IsSigmaCompact.image_of_continuousOn {f : X → Y} {s : Set X} (hs : IsSigmaCompact s)
    (hf : ContinuousOn f s) : IsSigmaCompact (f '' s) := by
  rcases hs with ⟨K, hcompact, hcov⟩
  refine ⟨fun n ↦ f '' K n, ?_, hcov.symm ▸ image_iUnion.symm⟩
  exact fun n ↦ (hcompact n).image_of_continuousOn (hf.mono (hcov.symm ▸ subset_iUnion K n))
Continuous image of a $\sigma$-compact set is $\sigma$-compact
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a $\sigma$-compact subset, and $f : X \to Y$ a function that is continuous on $s$. Then the image $f(s)$ is $\sigma$-compact in $Y$.
IsSigmaCompact.image theorem
{f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsSigmaCompact s) : IsSigmaCompact (f '' s)
Full source 
/-- If `s` is σ-compact and `f` continuous, `f(s)` is σ-compact. -/
lemma IsSigmaCompact.image {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsSigmaCompact s) :
    IsSigmaCompact (f '' s) := hs.image_of_continuousOn hf.continuousOn
Continuous image of a $\sigma$-compact set is $\sigma$-compact
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ a $\sigma$-compact subset, and $f : X \to Y$ a continuous function. Then the image $f(s)$ is $\sigma$-compact in $Y$.
Topology.IsInducing.isSigmaCompact_iff theorem
{f : X → Y} {s : Set X} (hf : IsInducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
Full source 
/-- If `f : X → Y` is an inducing map, the image `f '' s` of a set `s` is σ-compact
  if and only `s` is σ-compact. -/
lemma Topology.IsInducing.isSigmaCompact_iff {f : X → Y} {s : Set X}
    (hf : IsInducing f) : IsSigmaCompactIsSigmaCompact s ↔ IsSigmaCompact (f '' s) := by
  constructor
  · exact fun h ↦ h.image hf.continuous
  · rintro ⟨L, hcomp, hcov⟩
    -- Suppose f(s) is σ-compact; we want to show s is σ-compact.
    -- Write f(s) as a union of compact sets L n, so s = ⋃ K n with K n := f⁻¹(L n) ∩ s.
    -- Since f is inducing, each K n is compact iff L n is.
    refine ⟨fun n ↦ f ⁻¹' (L n) ∩ s, ?_, ?_⟩
    · intro n
      have : f '' (f ⁻¹' (L n) ∩ s) = L n := by
        rw [image_preimage_inter, inter_eq_left.mpr]
        exact (subset_iUnion _ n).trans hcov.le
      apply hf.isCompact_iff.mpr (this.symm ▸ (hcomp n))
    · calc ⋃ n, f ⁻¹' L n ∩ s
        _ = f ⁻¹' (⋃ n, L n)f ⁻¹' (⋃ n, L n) ∩ s  := by rw [preimage_iUnion, iUnion_inter]
        _ = f ⁻¹' (f '' s)f ⁻¹' (f '' s) ∩ s := by rw [hcov]
        _ = s := inter_eq_right.mpr (subset_preimage_image _ _)
$\sigma$-compactness under inducing maps: $s$ is $\sigma$-compact iff $f(s)$ is $\sigma$-compact
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an inducing map, and $s \subseteq X$ a subset. Then $s$ is $\sigma$-compact if and only if its image $f(s)$ is $\sigma$-compact.
Topology.IsEmbedding.isSigmaCompact_iff theorem
{f : X → Y} {s : Set X} (hf : IsEmbedding f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)
Full source 
/-- If `f : X → Y` is an embedding, the image `f '' s` of a set `s` is σ-compact
if and only `s` is σ-compact. -/
lemma Topology.IsEmbedding.isSigmaCompact_iff {f : X → Y} {s : Set X}
    (hf : IsEmbedding f) : IsSigmaCompactIsSigmaCompact s ↔ IsSigmaCompact (f '' s) :=
  hf.isInducing.isSigmaCompact_iff
$\sigma$-compactness under embeddings: $s$ is $\sigma$-compact iff $f(s)$ is $\sigma$-compact
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ an embedding, and $s \subseteq X$ a subset. Then $s$ is $\sigma$-compact if and only if its image $f(s)$ is $\sigma$-compact.
Subtype.isSigmaCompact_iff theorem
{p : X → Prop} {s : Set { a // p a }} : IsSigmaCompact s ↔ IsSigmaCompact ((↑) '' s : Set X)
Full source 
/-- Sets of subtype are σ-compact iff the image under a coercion is. -/
lemma Subtype.isSigmaCompact_iff {p : X → Prop} {s : Set { a // p a }} :
    IsSigmaCompactIsSigmaCompact s ↔ IsSigmaCompact ((↑) '' s : Set X) :=
  IsEmbedding.subtypeVal.isSigmaCompact_iff
$\sigma$-compactness of a subset in a subtype is equivalent to $\sigma$-compactness of its image in the ambient space
Informal description
Let $X$ be a topological space and $p : X \to \text{Prop}$ a predicate on $X$. For any subset $s$ of the subtype $\{a \in X \mid p(a)\}$, $s$ is $\sigma$-compact if and only if its image under the canonical inclusion map $\{a \in X \mid p(a)\} \hookrightarrow X$ is $\sigma$-compact in $X$.
SigmaCompactSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- A σ-compact space is a space that is the union of a countable collection of compact subspaces.
  Note that a locally compact separable T₂ space need not be σ-compact.
  The sequence can be extracted using `compactCovering`. -/
class SigmaCompactSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a σ-compact space, `Set.univ` is a σ-compact set. -/
  isSigmaCompact_univ : IsSigmaCompact (univ : Set X)
σ-Compact Space
Informal description
A topological space \( X \) is called σ-compact if it can be expressed as the union of a countable collection of compact subspaces. Note that a locally compact separable Hausdorff space is not necessarily σ-compact. The sequence of compact subspaces can be extracted using the function `compactCovering`.
isSigmaCompact_univ_iff theorem
: IsSigmaCompact (univ : Set X) ↔ SigmaCompactSpace X
Full source 
/-- A topological space is σ-compact iff `univ` is σ-compact. -/
lemma isSigmaCompact_univ_iff : IsSigmaCompactIsSigmaCompact (univ : Set X) ↔ SigmaCompactSpace X :=
  ⟨fun h => ⟨h⟩, fun h => h.1⟩
Characterization of $\sigma$-compact spaces via $\sigma$-compactness of the whole space
Informal description
A topological space $X$ is $\sigma$-compact if and only if the entire space (as a subset) is $\sigma$-compact, i.e., there exists a countable family of compact subsets $K_n \subseteq X$ such that $X = \bigcup_{n} K_n$.
isSigmaCompact_univ theorem
[h : SigmaCompactSpace X] : IsSigmaCompact (univ : Set X)
Full source 
/-- In a σ-compact space, `univ` is σ-compact. -/
lemma isSigmaCompact_univ [h : SigmaCompactSpace X] : IsSigmaCompact (univ : Set X) :=
  isSigmaCompact_univ_iff.mpr h
$\sigma$-compactness of the entire space in a $\sigma$-compact space
Informal description
If $X$ is a $\sigma$-compact topological space, then the entire space $X$ is $\sigma$-compact, i.e., there exists a countable family of compact subsets $K_n \subseteq X$ such that $X = \bigcup_{n} K_n$.
SigmaCompactSpace_iff_exists_compact_covering theorem
: SigmaCompactSpace X ↔ ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ
Full source 
/-- A topological space is σ-compact iff there exists a countable collection of compact
subspaces that cover the entire space. -/
lemma SigmaCompactSpace_iff_exists_compact_covering :
    SigmaCompactSpaceSigmaCompactSpace X ↔ ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ := by
  rw [← isSigmaCompact_univ_iff, IsSigmaCompact]
Characterization of $\sigma$-compact spaces via countable compact cover
Informal description
A topological space $X$ is $\sigma$-compact if and only if there exists a sequence of compact subsets $(K_n)_{n \in \mathbb{N}}$ such that $X = \bigcup_{n \in \mathbb{N}} K_n$.
SigmaCompactSpace.exists_compact_covering theorem
[h : SigmaCompactSpace X] : ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ
Full source 
lemma SigmaCompactSpace.exists_compact_covering [h : SigmaCompactSpace X] :
    ∃ K : ℕ → Set X, (∀ n, IsCompact (K n)) ∧ ⋃ n, K n = univ :=
  SigmaCompactSpace_iff_exists_compact_covering.mp h
Existence of Compact Covering for $\sigma$-Compact Spaces
Informal description
If $X$ is a $\sigma$-compact topological space, then there exists a sequence of compact subsets $(K_n)_{n \in \mathbb{N}}$ such that $X = \bigcup_{n \in \mathbb{N}} K_n$.
isSigmaCompact_range theorem
{f : X → Y} (hf : Continuous f) [SigmaCompactSpace X] : IsSigmaCompact (range f)
Full source 
/-- If `X` is σ-compact, `im f` is σ-compact. -/
lemma isSigmaCompact_range {f : X → Y} (hf : Continuous f) [SigmaCompactSpace X] :
    IsSigmaCompact (range f) :=
  image_univ ▸ isSigmaCompact_univ.image hf
Continuous image of a $\sigma$-compact space is $\sigma$-compact
Informal description
Let $X$ be a $\sigma$-compact topological space and $Y$ another topological space. For any continuous function $f \colon X \to Y$, the range of $f$ is $\sigma$-compact in $Y$.
isSigmaCompact_iff_isSigmaCompact_univ theorem
{s : Set X} : IsSigmaCompact s ↔ IsSigmaCompact (univ : Set s)
Full source 
/-- A subset `s` is σ-compact iff `s` (with the subspace topology) is a σ-compact space. -/
lemma isSigmaCompact_iff_isSigmaCompact_univ {s : Set X} :
    IsSigmaCompactIsSigmaCompact s ↔ IsSigmaCompact (univ : Set s) := by
  rw [Subtype.isSigmaCompact_iff, image_univ, Subtype.range_coe]
$\sigma$-compactness of a subset is equivalent to $\sigma$-compactness of the subspace
Informal description
A subset $s$ of a topological space $X$ is $\sigma$-compact if and only if the subspace $s$ (equipped with the subspace topology) is a $\sigma$-compact space.
isSigmaCompact_iff_sigmaCompactSpace theorem
{s : Set X} : IsSigmaCompact s ↔ SigmaCompactSpace s
Full source 
lemma isSigmaCompact_iff_sigmaCompactSpace {s : Set X} :
    IsSigmaCompactIsSigmaCompact s ↔ SigmaCompactSpace s :=
  isSigmaCompact_iff_isSigmaCompact_univ.trans isSigmaCompact_univ_iff
$\sigma$-compact subset iff subspace is $\sigma$-compact
Informal description
A subset $s$ of a topological space $X$ is $\sigma$-compact if and only if the subspace $s$ (equipped with the subspace topology) is a $\sigma$-compact space.
SigmaCompactSpace.of_countable theorem
(S : Set (Set X)) (Hc : S.Countable) (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = univ) : SigmaCompactSpace X
Full source 
theorem SigmaCompactSpace.of_countable (S : Set (Set X)) (Hc : S.Countable)
    (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = univ) : SigmaCompactSpace X :=
  ⟨(exists_seq_cover_iff_countable ⟨_, isCompact_empty⟩).2 ⟨S, Hc, Hcomp, HU⟩⟩
Countable Union of Compact Sets Implies σ-Compactness
Informal description
Let \( X \) be a topological space and \( S \) be a countable collection of subsets of \( X \). If every set in \( S \) is compact and the union of all sets in \( S \) is the entire space \( X \), then \( X \) is σ-compact.
sigmaCompactSpace_of_locallyCompact_secondCountable instance
[LocallyCompactSpace X] [SecondCountableTopology X] : SigmaCompactSpace X
Full source 
instance (priority := 100) sigmaCompactSpace_of_locallyCompact_secondCountable
    [LocallyCompactSpace X] [SecondCountableTopology X] : SigmaCompactSpace X := by
  choose K hKc hxK using fun x : X => exists_compact_mem_nhds x
  rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩
  refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
  rwa [sUnion_image]
Second-Countable Locally Compact Spaces are σ-Compact
Informal description
Every second-countable locally compact topological space is σ-compact.
compactCovering definition
: ℕ → Set X
Full source 
/-- A choice of compact covering for a `σ`-compact space, chosen to be monotone. -/
def compactCovering : ℕ → Set X :=
  Accumulate exists_compact_covering.choose
Compact covering of a σ-compact space
Informal description
A monotone sequence of compact subsets of a σ-compact topological space \( X \) whose union is the entire space. Specifically, for each natural number \( n \), the set \( K_n \) is compact, and \( X = \bigcup_{n \in \mathbb{N}} K_n \).
isCompact_compactCovering theorem
(n : ℕ) : IsCompact (compactCovering X n)
Full source 
theorem isCompact_compactCovering (n : ℕ) : IsCompact (compactCovering X n) :=
  isCompact_accumulate (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).1 n
Compactness of the $n$-th Set in a $\sigma$-Compact Space's Covering
Informal description
For every natural number $n$, the subset $K_n$ of the $\sigma$-compact topological space $X$ (where $K_n$ is the $n$-th set in the compact covering sequence) is compact.
iUnion_compactCovering theorem
: ⋃ n, compactCovering X n = univ
Full source 
theorem iUnion_compactCovering : ⋃ n, compactCovering X n = univ := by
  rw [compactCovering, iUnion_accumulate]
  exact (Classical.choose_spec SigmaCompactSpace.exists_compact_covering).2
Union of Compact Covering Equals Space in σ-Compact Topological Space
Informal description
The union of the compact covering sets $(K_n)_{n \in \mathbb{N}}$ of a σ-compact topological space $X$ equals the entire space, i.e., $\bigcup_{n \in \mathbb{N}} K_n = X$.
iUnion_closure_compactCovering theorem
: ⋃ n, closure (compactCovering X n) = univ
Full source 
theorem iUnion_closure_compactCovering : ⋃ n, closure (compactCovering X n) = univ :=
  eq_top_mono (iUnion_mono fun _ ↦ subset_closure) (iUnion_compactCovering X)
Union of Closures of Compact Covering Equals Space in σ-Compact Space
Informal description
For a σ-compact topological space $X$, the union of the closures of the compact covering sets $(K_n)_{n \in \mathbb{N}}$ equals the entire space, i.e., $\bigcup_{n \in \mathbb{N}} \overline{K_n} = X$.
compactCovering_subset theorem
⦃m n : ℕ⦄ (h : m ≤ n) : compactCovering X m ⊆ compactCovering X n
Full source 
@[mono, gcongr]
theorem compactCovering_subset ⦃m n : ℕ⦄ (h : m ≤ n) : compactCoveringcompactCovering X m ⊆ compactCovering X n :=
  monotone_accumulate h
Monotonicity of Compact Covering in $\sigma$-Compact Spaces
Informal description
For any natural numbers $m$ and $n$ with $m \leq n$, the compact subset $K_m$ in the compact covering of a $\sigma$-compact space $X$ is contained in the compact subset $K_n$, i.e., $K_m \subseteq K_n$.
exists_mem_compactCovering theorem
(x : X) : ∃ n, x ∈ compactCovering X n
Full source 
theorem exists_mem_compactCovering (x : X) : ∃ n, x ∈ compactCovering X n :=
  iUnion_eq_univ_iff.mp (iUnion_compactCovering X) x
Existence of Compact Covering Member for Every Point in $\sigma$-Compact Space
Informal description
For any point $x$ in a $\sigma$-compact topological space $X$, there exists a natural number $n$ such that $x$ belongs to the $n$-th compact set in the compact covering of $X$.
instSigmaCompactSpaceProd instance
[SigmaCompactSpace Y] : SigmaCompactSpace (X × Y)
Full source 
instance [SigmaCompactSpace Y] : SigmaCompactSpace (X × Y) :=
  ⟨⟨fun n => compactCovering X n ×ˢ compactCovering Y n, fun _ =>
      (isCompact_compactCovering _ _).prod (isCompact_compactCovering _ _), by
      simp only [iUnion_prod_of_monotone (compactCovering_subset X) (compactCovering_subset Y),
        iUnion_compactCovering, univ_prod_univ]⟩⟩
$\sigma$-Compactness of Product Spaces
Informal description
For any topological spaces $X$ and $Y$, if $Y$ is $\sigma$-compact, then the product space $X \times Y$ is also $\sigma$-compact.
instSigmaCompactSpaceForallOfFinite instance
[Finite ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SigmaCompactSpace (X i)] : SigmaCompactSpace (∀ i, X i)
Full source 
instance [Finite ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SigmaCompactSpace (X i)] :
    SigmaCompactSpace (∀ i, X i) := by
  refine ⟨⟨fun n => Set.pi univ fun i => compactCovering (X i) n,
    fun n => isCompact_univ_pi fun i => isCompact_compactCovering (X i) _, ?_⟩⟩
  rw [iUnion_univ_pi_of_monotone]
  · simp only [iUnion_compactCovering, pi_univ]
  · exact fun i => compactCovering_subset (X i)
$\sigma$-Compactness of Finite Product Spaces
Informal description
For any finite index set $\iota$ and a family of topological spaces $(X_i)_{i \in \iota}$ where each $X_i$ is $\sigma$-compact, the product space $\prod_{i \in \iota} X_i$ is also $\sigma$-compact.
instSigmaCompactSpaceSum instance
[SigmaCompactSpace Y] : SigmaCompactSpace (X ⊕ Y)
Full source 
instance [SigmaCompactSpace Y] : SigmaCompactSpace (X ⊕ Y) :=
  ⟨⟨fun n => Sum.inl '' compactCovering X n ∪ Sum.inr '' compactCovering Y n, fun n =>
      ((isCompact_compactCovering X n).image continuous_inl).union
        ((isCompact_compactCovering Y n).image continuous_inr),
      by simp only [iUnion_union_distrib, ← image_iUnion, iUnion_compactCovering, image_univ,
        range_inl_union_range_inr]⟩⟩
$\sigma$-Compactness of Disjoint Union with a $\sigma$-Compact Space
Informal description
For any two topological spaces $X$ and $Y$, if $Y$ is $\sigma$-compact, then the disjoint union $X \oplus Y$ is also $\sigma$-compact.
instSigmaCompactSpaceSigmaOfCountable instance
[Countable ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, SigmaCompactSpace (X i)] : SigmaCompactSpace (Σ i, X i)
Full source 
instance [Countable ι] {X : ι → Type*} [∀ i, TopologicalSpace (X i)]
    [∀ i, SigmaCompactSpace (X i)] : SigmaCompactSpace (Σi, X i) := by
  cases isEmpty_or_nonempty ι
  · infer_instance
  · rcases exists_surjective_nat ι with ⟨f, hf⟩
    refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩
    · refine (finite_le_nat _).isCompact_biUnion fun k _ => ?_
      exact (isCompact_compactCovering _ _).image continuous_sigmaMk
    · simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
      intro k y
      rcases exists_mem_compactCovering y with ⟨n, hn⟩
      refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
      exact compactCovering_subset _ (le_max_right _ _) hn
$\sigma$-Compactness of Countable Disjoint Union of $\sigma$-Compact Spaces
Informal description
For any countable index set $\iota$ and a family of topological spaces $(X_i)_{i \in \iota}$ where each $X_i$ is $\sigma$-compact, the disjoint union $\bigsqcup_{i \in \iota} X_i$ is also $\sigma$-compact.
Topology.IsClosedEmbedding.sigmaCompactSpace theorem
{e : Y → X} (he : IsClosedEmbedding e) : SigmaCompactSpace Y
Full source 
protected lemma Topology.IsClosedEmbedding.sigmaCompactSpace {e : Y → X}
    (he : IsClosedEmbedding e) : SigmaCompactSpace Y :=
  ⟨⟨fun n => e ⁻¹' compactCovering X n, fun _ =>
      he.isCompact_preimage (isCompact_compactCovering _ _), by
      rw [← preimage_iUnion, iUnion_compactCovering, preimage_univ]⟩⟩
$\sigma$-Compactness is Preserved Under Closed Embeddings
Informal description
Let $X$ and $Y$ be topological spaces, and let $e: Y \to X$ be a closed embedding. Then $Y$ is $\sigma$-compact.
LocallyFinite.countable_univ theorem
{f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Countable
Full source 
/-- If `X` is a `σ`-compact space, then a locally finite family of nonempty sets of `X` can have
only countably many elements, `Set.Countable` version. -/
protected theorem LocallyFinite.countable_univ {f : ι → Set X} (hf : LocallyFinite f)
    (hne : ∀ i, (f i).Nonempty) : (univ : Set ι).Countable := by
  have := fun n => hf.finite_nonempty_inter_compact (isCompact_compactCovering X n)
  refine (countable_iUnion fun n => (this n).countable).mono fun i _ => ?_
  rcases hne i with ⟨x, hx⟩
  rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering X) x with ⟨n, hn⟩
  exact mem_iUnion.2 ⟨n, x, hx, hn⟩
Countability of Locally Finite Nonempty Families in $\sigma$-Compact Spaces
Informal description
Let $X$ be a $\sigma$-compact topological space and $\{f_i\}_{i \in \iota}$ be a locally finite family of nonempty subsets of $X$. Then the index set $\iota$ is countable.
LocallyFinite.encodable definition
{ι : Type*} {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : Encodable ι
Full source 
/-- If `f : ι → Set X` is a locally finite covering of a σ-compact topological space by nonempty
sets, then the index type `ι` is encodable. -/
protected noncomputable def LocallyFinite.encodable {ι : Type*} {f : ι → Set X}
    (hf : LocallyFinite f) (hne : ∀ i, (f i).Nonempty) : Encodable ι :=
  @Encodable.ofEquiv _ _ (hf.countable_univ hne).toEncodable (Equiv.Set.univ _).symm
Encodability of locally finite nonempty families in $\sigma$-compact spaces
Informal description
Let $X$ be a $\sigma$-compact topological space and $\{f_i\}_{i \in \iota}$ be a locally finite family of nonempty subsets of $X$. Then the index type $\iota$ is encodable.
countable_cover_nhdsWithin_of_sigmaCompact theorem
{f : X → Set X} {s : Set X} (hs : IsClosed s) (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
Full source 
/-- In a topological space with sigma compact topology, if `f` is a function that sends each point
`x` of a closed set `s` to a neighborhood of `x` within `s`, then for some countable set `t ⊆ s`,
the neighborhoods `f x`, `x ∈ t`, cover the whole set `s`. -/
theorem countable_cover_nhdsWithin_of_sigmaCompact {f : X → Set X} {s : Set X} (hs : IsClosed s)
    (hf : ∀ x ∈ s, f x ∈ 𝓝[s] x) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x := by
  simp only [nhdsWithin, mem_inf_principal] at hf
  choose t ht hsub using fun n =>
    ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right
  refine
    ⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
      countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩
  rcases exists_mem_compactCovering x with ⟨n, hn⟩
  rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
  exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩
Countable Covering Theorem for Closed Sets in $\sigma$-Compact Spaces
Informal description
Let $X$ be a $\sigma$-compact topological space, $s$ a closed subset of $X$, and $f$ a function assigning to each $x \in s$ a neighborhood $f(x)$ of $x$ within $s$. Then there exists a countable subset $t \subseteq s$ such that the neighborhoods $\{f(x)\}_{x \in t}$ cover $s$.
countable_cover_nhds_of_sigmaCompact theorem
{f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) : ∃ s : Set X, s.Countable ∧ ⋃ x ∈ s, f x = univ
Full source 
/-- In a topological space with sigma compact topology, if `f` is a function that sends each
point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
`x ∈ s`, cover the whole space. -/
theorem countable_cover_nhds_of_sigmaCompact {f : X → Set X} (hf : ∀ x, f x ∈ 𝓝 x) :
    ∃ s : Set X, s.Countable ∧ ⋃ x ∈ s, f x = univ := by
  simp only [← nhdsWithin_univ] at hf
  rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩
  exact ⟨s, hsc, univ_subset_iff.1 hsU⟩
Countable Covering Theorem for $\sigma$-Compact Spaces
Informal description
Let $X$ be a $\sigma$-compact topological space and $f$ a function assigning to each $x \in X$ a neighborhood $f(x)$ of $x$. Then there exists a countable subset $s \subseteq X$ such that the neighborhoods $\{f(x)\}_{x \in s}$ cover $X$.
CompactExhaustion structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- An [exhaustion by compact sets](https://en.wikipedia.org/wiki/Exhaustion_by_compact_sets) of a
topological space is a sequence of compact sets `K n` such that `K n ⊆ interior (K (n + 1))` and
`⋃ n, K n = univ`.

If `X` is a locally compact sigma compact space, then `CompactExhaustion.choice X` provides
a choice of an exhaustion by compact sets. This choice is also available as
`(default : CompactExhaustion X)`. -/
structure CompactExhaustion (X : Type*) [TopologicalSpace X] where
  /-- The sequence of compact sets that form a compact exhaustion. -/
  toFun : ℕ → Set X
  /-- The sets in the compact exhaustion are in fact compact. -/
  isCompact' : ∀ n, IsCompact (toFun n)
  /-- The sets in the compact exhaustion form a sequence:
    each set is contained in the interior of the next. -/
  subset_interior_succ' : ∀ n, toFun n ⊆ interior (toFun (n + 1))
  /-- The union of all sets in a compact exhaustion equals the entire space. -/
  iUnion_eq' : ⋃ n, toFun n = univ
Exhaustion by compact sets
Informal description
An exhaustion by compact sets of a topological space $X$ is a sequence of compact subsets $(K_n)_{n \in \mathbb{N}}$ such that: 1. $K_n \subseteq \text{interior}(K_{n+1})$ for all $n \in \mathbb{N}$, 2. $\bigcup_{n \in \mathbb{N}} K_n = X$. If $X$ is a locally compact $\sigma$-compact space, then there exists a choice of such an exhaustion by compact sets, which can be obtained via `CompactExhaustion.choice X` or as the default instance `(default : CompactExhaustion X)`.
CompactExhaustion.instFunLikeNatSet instance
: FunLike (CompactExhaustion X) ℕ (Set X)
Full source 
instance : FunLike (CompactExhaustion X) ℕ (Set X) where
  coe := toFun
  coe_injective' | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl
Function-Like Structure of Compact Exhaustions
Informal description
For any topological space $X$, the type `CompactExhaustion X` of exhaustions by compact sets can be treated as a function-like type from natural numbers to subsets of $X$.
CompactExhaustion.instRelHomClassNatSetLeSubset instance
: RelHomClass (CompactExhaustion X) LE.le HasSubset.Subset
Full source 
instance : RelHomClass (CompactExhaustion X) LE.le HasSubset.Subset where
  map_rel f _ _ h := monotone_nat_of_le_succ
    (fun n ↦ (f.subset_interior_succ' n).trans interior_subset) h
Monotonicity of Compact Exhaustion Sets
Informal description
For any topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, the sequence $K_n$ is monotone with respect to inclusion, meaning $K_n \subseteq K_{n+1}$ for all $n \in \mathbb{N}$.
CompactExhaustion.toFun_eq_coe theorem
: K.toFun = K
Full source 
@[simp]
theorem toFun_eq_coe : K.toFun = K := rfl
Equality of Compact Exhaustion Function and Its Representation
Informal description
For any compact exhaustion $K$ of a topological space $X$, the function `toFun` associated with $K$ is equal to $K$ itself.
CompactExhaustion.isCompact theorem
(n : ℕ) : IsCompact (K n)
Full source 
protected theorem isCompact (n : ℕ) : IsCompact (K n) :=
  K.isCompact' n
Compactness of Exhaustion Sets: $K_n$ is compact for all $n \in \mathbb{N}$
Informal description
For any natural number $n$, the subset $K_n$ of the topological space $X$ is compact.
CompactExhaustion.subset_interior_succ theorem
(n : ℕ) : K n ⊆ interior (K (n + 1))
Full source 
theorem subset_interior_succ (n : ℕ) : K n ⊆ interior (K (n + 1)) :=
  K.subset_interior_succ' n
Nested Interior Property of Compact Exhaustion: $K_n \subseteq \text{interior}(K_{n+1})$
Informal description
For any natural number $n$, the compact subset $K_n$ of the topological space $X$ is contained in the interior of the next subset $K_{n+1}$ in the exhaustion sequence, i.e., $K_n \subseteq \text{interior}(K_{n+1})$.
CompactExhaustion.subset theorem
⦃m n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n
Full source 
@[mono]
protected theorem subset ⦃m n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n :=
  OrderHomClass.mono K h
Monotonicity of Compact Exhaustion: $K_m \subseteq K_n$ for $m \leq n$
Informal description
For any natural numbers $m$ and $n$ with $m \leq n$, the compact subset $K_m$ of the topological space $X$ is contained in the compact subset $K_n$.
CompactExhaustion.subset_succ theorem
(n : ℕ) : K n ⊆ K (n + 1)
Full source 
theorem subset_succ (n : ℕ) : K n ⊆ K (n + 1) := K.subset n.le_succ
Monotonicity of Compact Exhaustion: $K_n \subseteq K_{n+1}$
Informal description
For any natural number $n$, the compact subset $K_n$ in a compact exhaustion of a topological space $X$ is contained in the next subset $K_{n+1}$, i.e., $K_n \subseteq K_{n+1}$.
CompactExhaustion.subset_interior theorem
⦃m n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n)
Full source 
theorem subset_interior ⦃m n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n) :=
  Subset.trans (K.subset_interior_succ m) <| interior_mono <| K.subset h
Nested Interior Property of Compact Exhaustion for $m < n$: $K_m \subseteq \text{interior}(K_n)$
Informal description
For any natural numbers $m$ and $n$ with $m < n$, the compact subset $K_m$ of a topological space $X$ is contained in the interior of the subset $K_n$ in the exhaustion sequence, i.e., $K_m \subseteq \text{interior}(K_n)$.
CompactExhaustion.iUnion_eq theorem
: ⋃ n, K n = univ
Full source 
theorem iUnion_eq : ⋃ n, K n = univ :=
  K.iUnion_eq'
Union of Compact Exhaustion Covers the Space
Informal description
For a compact exhaustion $(K_n)_{n \in \mathbb{N}}$ of a topological space $X$, the union of all $K_n$ equals the entire space $X$, i.e., $\bigcup_{n \in \mathbb{N}} K_n = X$.
CompactExhaustion.exists_mem theorem
(x : X) : ∃ n, x ∈ K n
Full source 
theorem exists_mem (x : X) : ∃ n, x ∈ K n :=
  iUnion_eq_univ_iff.1 K.iUnion_eq x
Existence of Compact Set Containing Any Point in a Compact Exhaustion
Informal description
For any point $x$ in a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, there exists a natural number $n$ such that $x \in K_n$.
CompactExhaustion.exists_mem_nhds theorem
(x : X) : ∃ n, K n ∈ 𝓝 x
Full source 
theorem exists_mem_nhds (x : X) : ∃ n, K n ∈ 𝓝 x := by
  rcases K.exists_mem x with ⟨n, hn⟩
  exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩
Existence of Compact Neighborhood in Compact Exhaustion
Informal description
For any point $x$ in a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, there exists a natural number $n$ such that $K_n$ is a neighborhood of $x$.
CompactExhaustion.exists_superset_of_isCompact theorem
{s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n
Full source 
/-- A compact exhaustion eventually covers any compact set. -/
theorem exists_superset_of_isCompact {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n := by
  suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
  refine hs.elim_directed_cover (interiorinterior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
  · intro x _
    rcases K.exists_mem x with ⟨k, hk⟩
    exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩
  · exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h
Compact Exhaustion Covers Any Compact Set
Informal description
For any compact subset $s$ of a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, there exists a natural number $n$ such that $s \subseteq K_n$.
CompactExhaustion.find definition
(x : X) : ℕ
Full source 
/-- The minimal `n` such that `x ∈ K n`. -/
protected noncomputable def find (x : X) : ℕ :=
  Nat.find (K.exists_mem x)
Minimal index of a compact set containing a point
Informal description
For a topological space \( X \) with a compact exhaustion \( (K_n)_{n \in \mathbb{N}} \), the function \( \text{find} \) maps each point \( x \in X \) to the minimal natural number \( n \) such that \( x \in K_n \).
CompactExhaustion.mem_find theorem
(x : X) : x ∈ K (K.find x)
Full source 
theorem mem_find (x : X) : x ∈ K (K.find x) := by
  classical
  exact Nat.find_spec (K.exists_mem x)
Minimal Compact Set Contains Point in Compact Exhaustion
Informal description
For any point $x$ in a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, the point $x$ belongs to the compact set $K_n$ where $n$ is the minimal index given by the function $\text{find}(x)$.
CompactExhaustion.mem_iff_find_le theorem
{x : X} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n
Full source 
theorem mem_iff_find_le {x : X} {n : ℕ} : x ∈ K nx ∈ K n ↔ K.find x ≤ n := by
  classical
  exact ⟨fun h => Nat.find_min' (K.exists_mem x) h, fun h => K.subset h <| K.mem_find x⟩
Characterization of Membership in Compact Exhaustion via Minimal Index
Informal description
For a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, a point $x \in X$ belongs to the compact set $K_n$ if and only if the minimal index $m$ such that $x \in K_m$ (given by $K.\text{find}(x)$) satisfies $m \leq n$.
CompactExhaustion.shiftr definition
: CompactExhaustion X
Full source 
/-- Prepend the empty set to a compact exhaustion `K n`. -/
def shiftr : CompactExhaustion X where
  toFun n := Nat.casesOn n ∅ K
  isCompact' n := Nat.casesOn n isCompact_empty K.isCompact
  subset_interior_succ' n := Nat.casesOn n (empty_subset _) K.subset_interior_succ
  iUnion_eq' := iUnion_eq_univ_iff.2 fun x => ⟨K.find x + 1, K.mem_find x⟩
Shifted compact exhaustion
Informal description
Given a compact exhaustion $(K_n)_{n \in \mathbb{N}}$ of a topological space $X$, the shifted compact exhaustion $\text{shiftr}(K)$ is defined by: - $\text{shiftr}(K)(0) = \emptyset$, - $\text{shiftr}(K)(n+1) = K_n$ for all $n \in \mathbb{N}$. This shifted exhaustion satisfies: 1. Each $\text{shiftr}(K)(n)$ is compact, 2. $\text{shiftr}(K)(n) \subseteq \text{interior}(\text{shiftr}(K)(n+1))$ for all $n \in \mathbb{N}$, 3. $\bigcup_{n \in \mathbb{N}} \text{shiftr}(K)(n) = X$.
CompactExhaustion.find_shiftr theorem
(x : X) : K.shiftr.find x = K.find x + 1
Full source 
@[simp]
theorem find_shiftr (x : X) : K.shiftr.find x = K.find x + 1 := by
  classical
  exact Nat.find_comp_succ _ _ (not_mem_empty _)
Relation Between Find Indices in Original and Shifted Compact Exhaustions
Informal description
For any point $x$ in a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, the minimal index $n$ such that $x$ belongs to the shifted exhaustion $\text{shiftr}(K)(n)$ is equal to $K.\text{find}(x) + 1$.
CompactExhaustion.mem_diff_shiftr_find theorem
(x : X) : x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x)
Full source 
theorem mem_diff_shiftr_find (x : X) : x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x) :=
  ⟨K.mem_find _,
    mt K.shiftr.mem_iff_find_le.1 <| by simp only [find_shiftr, not_le, Nat.lt_succ_self]⟩
Point Belongs to Difference of Successive Compact Sets in Exhaustion
Informal description
For any point $x$ in a topological space $X$ with a compact exhaustion $(K_n)_{n \in \mathbb{N}}$, the point $x$ belongs to the set difference $K_{n+1} \setminus K_n$, where $n = K.\text{find}(x)$ is the minimal index such that $x \in K_n$.
CompactExhaustion.choice definition
(X : Type*) [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] : CompactExhaustion X
Full source 
/-- 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⟩
Construction of an exhaustion by compact sets for a \(\sigma\)-compact space
Informal description
Given a topological space \( X \) that is weakly locally compact and \(\sigma\)-compact, the function `CompactExhaustion.choice X` constructs an exhaustion by compact sets for \( X \). This exhaustion consists of a sequence of compact subsets \((K_n)_{n \in \mathbb{N}}\) such that: 1. \( K_n \subseteq \text{interior}(K_{n+1}) \) for all \( n \in \mathbb{N} \), 2. \(\bigcup_{n \in \mathbb{N}} K_n = X \).
CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfWeaklyLocallyCompactSpace instance
[SigmaCompactSpace X] [WeaklyLocallyCompactSpace X] : Inhabited (CompactExhaustion X)
Full source 
noncomputable instance [SigmaCompactSpace X] [WeaklyLocallyCompactSpace X] :
    Inhabited (CompactExhaustion X) :=
  ⟨CompactExhaustion.choice X⟩
Existence of Compact Exhaustion for $\sigma$-Compact Spaces
Informal description
For any topological space $X$ that is $\sigma$-compact and weakly locally compact, there exists a default exhaustion by compact sets.