# Documentation

Mathlib.Topology.Compactness.SigmaCompact

# 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.
def IsSigmaCompact {X : Type u_1} [] (s : Set X) :

A subset s ⊆ X is called σ-compact if it is the union of countably many compact sets.

Equations
Instances For
theorem IsCompact.isSigmaCompact {X : Type u_1} [] {s : Set X} (hs : ) :

Compact sets are σ-compact.

@[simp]
theorem isSigmaCompact_empty {X : Type u_1} [] :

The empty set is σ-compact.

theorem isSigmaCompact_iUnion_of_isCompact {X : Type u_1} {ι : Type u_3} [] [hι : ] (s : ιSet X) (hcomp : ∀ (i : ι), IsCompact (s i)) :
IsSigmaCompact (⋃ (i : ι), s i)

Countable unions of compact sets are σ-compact.

theorem isSigmaCompact_sUnion_of_isCompact {X : Type u_1} [] {S : Set (Set X)} (hc : ) (hcomp : sS, ) :

Countable unions of compact sets are σ-compact.

theorem isSigmaCompact_iUnion {X : Type u_1} {ι : Type u_3} [] [] (s : ιSet X) (hcomp : ∀ (i : ι), IsSigmaCompact (s i)) :
IsSigmaCompact (⋃ (i : ι), s i)

Countable unions of σ-compact sets are σ-compact.

theorem isSigmaCompact_sUnion {X : Type u_1} [] (S : Set (Set X)) (hc : ) (hcomp : ∀ (s : S), ) :

Countable unions of σ-compact sets are σ-compact.

theorem isSigmaCompact_biUnion {X : Type u_1} {ι : Type u_3} [] {s : Set ι} {S : ιSet X} (hc : ) (hcomp : is, IsSigmaCompact (S i)) :
IsSigmaCompact (⋃ i ∈ s, S i)

Countable unions of σ-compact sets are σ-compact.

theorem IsSigmaCompact.of_isClosed_subset {X : Type u_1} [] {s : Set X} {t : Set X} (ht : ) (hs : ) (h : s t) :

A closed subset of a σ-compact set is σ-compact.

theorem IsSigmaCompact.image_of_continuousOn {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hs : ) (hf : ) :

If s is σ-compact and f is continuous on s, f(s) is σ-compact.

theorem IsSigmaCompact.image {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) {s : Set X} (hs : ) :

If s is σ-compact and f continuous, f(s) is σ-compact.

theorem Inducing.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) :

If f : X → Y is Inducing, the image f '' s of a set s is σ-compact if and only s is σ-compact.

theorem Embedding.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (hf : ) :

If f : X → Y is an Embedding, the image f '' s of a set s is σ-compact if and only s is σ-compact.

theorem Subtype.isSigmaCompact_iff {X : Type u_1} [] {p : XProp} {s : Set { a : X // p a }} :
IsSigmaCompact (Subtype.val '' s)

Sets of subtype are σ-compact iff the image under a coercion is.

class SigmaCompactSpace (X : Type u_4) [] :

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.

• isSigmaCompact_univ : IsSigmaCompact Set.univ

In a σ-compact space, Set.univ is a σ-compact set.

Instances
theorem isSigmaCompact_univ_iff {X : Type u_1} [] :

A topological space is σ-compact iff univ is σ-compact.

theorem isSigmaCompact_univ {X : Type u_1} [] [h : ] :

In a σ-compact space, univ is σ-compact.

theorem SigmaCompactSpace_iff_exists_compact_covering {X : Type u_1} [] :
∃ (K : Set X), (∀ (n : ), IsCompact (K n)) ⋃ (n : ), K n = Set.univ

A topological space is σ-compact iff there exists a countable collection of compact subspaces that cover the entire space.

theorem SigmaCompactSpace.exists_compact_covering {X : Type u_1} [] [h : ] :
∃ (K : Set X), (∀ (n : ), IsCompact (K n)) ⋃ (n : ), K n = Set.univ
theorem isSigmaCompact_range {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :

If X is σ-compact, im f is σ-compact.

theorem isSigmaCompact_iff_isSigmaCompact_univ {X : Type u_1} [] {s : Set X} :

A subset s is σ-compact iff s (with the subspace topology) is a σ-compact space.

theorem isSigmaCompact_iff_sigmaCompactSpace {X : Type u_1} [] {s : Set X} :
instance CompactSpace.sigma_compact {X : Type u_1} [] [] :
Equations
• (_ : ) = (_ : )
theorem SigmaCompactSpace.of_countable {X : Type u_1} [] (S : Set (Set X)) (Hc : ) (Hcomp : sS, ) (HU : ⋃₀ S = Set.univ) :
Equations
• (_ : ) = (_ : )
def compactCovering (X : Type u_1) [] :
Set X

A choice of compact covering for a σ-compact space, chosen to be monotone.

Equations
Instances For
theorem isCompact_compactCovering (X : Type u_1) [] (n : ) :
theorem iUnion_compactCovering (X : Type u_1) [] :
⋃ (n : ), = Set.univ
theorem compactCovering_subset (X : Type u_1) [] ⦃m : ⦃n : (h : m n) :
theorem exists_mem_compactCovering {X : Type u_1} [] (x : X) :
∃ (n : ), x
Equations
instance instSigmaCompactSpaceForAllTopologicalSpace {ι : Type u_3} [] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] :
SigmaCompactSpace ((i : ι) → X i)
Equations
Equations
instance instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_3} [] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] :
SigmaCompactSpace ((i : ι) × X i)
Equations
theorem ClosedEmbedding.sigmaCompactSpace {X : Type u_1} {Y : Type u_2} [] [] {e : YX} (he : ) :
theorem IsClosed.sigmaCompactSpace {X : Type u_1} [] {s : Set X} (hs : ) :
theorem LocallyFinite.countable_univ {X : Type u_1} {ι : Type u_3} [] {f : ιSet X} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :
Set.Countable Set.univ

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.

noncomputable def LocallyFinite.encodable {X : Type u_1} [] {ι : Type u_4} {f : ιSet X} (hf : ) (hne : ∀ (i : ι), Set.Nonempty (f i)) :

If f : ι → Set X is a locally finite covering of a σ-compact topological space by nonempty sets, then the index type ι is encodable.

Equations
Instances For
theorem countable_cover_nhdsWithin_of_sigma_compact {X : Type u_1} [] {f : XSet X} {s : Set X} (hs : ) (hf : xs, f x ) :
∃ (t : Set X) (_ : t s), s ⋃ x ∈ t, f x

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_nhds_of_sigma_compact {X : Type u_1} [] {f : XSet X} (hf : ∀ (x : X), f x nhds x) :
∃ (s : Set X), ⋃ x ∈ s, f x = Set.univ

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.

structure CompactExhaustion (X : Type u_4) [] :
Type u_4

An 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).

• toFun : Set X

The sequence of compact sets that form a compact exhaustion.

• isCompact' : ∀ (n : ),

The sets in the compact exhaustion are in fact compact.

• subset_interior_succ' : ∀ (n : ), interior (CompactExhaustion.toFun s (n + 1))

The sets in the compact exhaustion form a sequence: each set is contained in the interior of the next.

• iUnion_eq' : ⋃ (n : ), = Set.univ

The union of all sets in a compact exhaustion equals the entire space.

Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CompactExhaustion.toFun_eq_coe {X : Type u_1} [] (K : ) :
K.toFun = K
theorem CompactExhaustion.isCompact {X : Type u_1} [] (K : ) (n : ) :
IsCompact (K n)
theorem CompactExhaustion.subset_interior_succ {X : Type u_1} [] (K : ) (n : ) :
K n interior (K (n + 1))
theorem CompactExhaustion.subset {X : Type u_1} [] (K : ) ⦃m : ⦃n : (h : m n) :
K m K n
theorem CompactExhaustion.subset_succ {X : Type u_1} [] (K : ) (n : ) :
K n K (n + 1)
theorem CompactExhaustion.subset_interior {X : Type u_1} [] (K : ) ⦃m : ⦃n : (h : m < n) :
K m interior (K n)
theorem CompactExhaustion.iUnion_eq {X : Type u_1} [] (K : ) :
⋃ (n : ), K n = Set.univ
theorem CompactExhaustion.exists_mem {X : Type u_1} [] (K : ) (x : X) :
∃ (n : ), x K n
noncomputable def CompactExhaustion.find {X : Type u_1} [] (K : ) (x : X) :

The minimal n such that x ∈ K n.

Equations
Instances For
theorem CompactExhaustion.mem_find {X : Type u_1} [] (K : ) (x : X) :
x K ()
theorem CompactExhaustion.mem_iff_find_le {X : Type u_1} [] (K : ) {x : X} {n : } :
x K n
def CompactExhaustion.shiftr {X : Type u_1} [] (K : ) :

Prepend the empty set to a compact exhaustion K n.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CompactExhaustion.find_shiftr {X : Type u_1} [] (K : ) (x : X) :
theorem CompactExhaustion.mem_diff_shiftr_find {X : Type u_1} [] (K : ) (x : X) :
x () \
noncomputable def CompactExhaustion.choice (X : Type u_4) [] :

A choice of an exhaustion by compact sets of a weakly locally compact σ-compact space.

Equations
Instances For
noncomputable instance CompactExhaustion.instInhabitedCompactExhaustion {X : Type u_1} [] :
Equations
• CompactExhaustion.instInhabitedCompactExhaustion = { default := }