# 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 : S.Countable) (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 : S.Countable) (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 : s.Countable) (hcomp : is, IsSigmaCompact (S i)) :
IsSigmaCompact (is, 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 SigmaCompactSpace.isSigmaCompact_univ {X : Type u_4} [] [self : ] :

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

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 200]
instance CompactSpace.sigma_compact {X : Type u_1} [] [] :
Equations
• =
theorem SigmaCompactSpace.of_countable {X : Type u_1} [] (S : Set (Set X)) (Hc : S.Countable) (Hcomp : sS, ) (HU : ⋃₀ S = Set.univ) :
@[instance 100]
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 iUnion_closure_compactCovering (X : Type u_1) [] :
⋃ (n : ), closure () = 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
instance instSigmaCompactSpaceProd {X : Type u_1} {Y : Type u_2} [] [] :
Equations
• =
instance instSigmaCompactSpaceForallOfFinite {ι : Type u_3} [] {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] :
SigmaCompactSpace ((i : ι) → X i)
Equations
• =
instance instSigmaCompactSpaceSum {X : Type u_1} {Y : Type u_2} [] [] :
Equations
• =
instance instSigmaCompactSpaceSigmaOfCountable {ι : 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 : ) :
Equations
• =
theorem LocallyFinite.countable_univ {X : Type u_1} {ι : Type u_3} [] {f : ιSet X} (hf : ) (hne : ∀ (i : ι), (f i).Nonempty) :
Set.univ.Countable

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 : ι), (f i).Nonempty) :

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 ) :
ts, t.Countable s xt, 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), s.Countable xs, 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 : ), IsCompact (self.toFun n)

The sets in the compact exhaustion are in fact compact.

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

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

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

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

Instances For
theorem CompactExhaustion.isCompact' {X : Type u_4} [] (self : ) (n : ) :
IsCompact (self.toFun n)

The sets in the compact exhaustion are in fact compact.

theorem CompactExhaustion.subset_interior_succ' {X : Type u_4} [] (self : ) (n : ) :
self.toFun n interior (self.toFun (n + 1))

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

theorem CompactExhaustion.iUnion_eq' {X : Type u_4} [] (self : ) :
⋃ (n : ), self.toFun n = Set.univ

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

Equations
• CompactExhaustion.instFunLikeNatSet = { coe := CompactExhaustion.toFun, coe_injective' := }
Equations
• =
@[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
theorem CompactExhaustion.exists_superset_of_isCompact {X : Type u_1} [] (K : ) {s : Set X} (hs : ) :
∃ (n : ), s K n

A compact exhaustion eventually covers any compact set.

noncomputable def CompactExhaustion.find {X : Type u_1} [] (K : ) (x : X) :

The minimal n such that x ∈ K n.

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

Prepend the empty set to a compact exhaustion K n.

Equations
• K.shiftr = { toFun := fun (n : ) => Nat.casesOn n K, isCompact' := , subset_interior_succ' := , iUnion_eq' := }
Instances For
@[simp]
theorem CompactExhaustion.find_shiftr {X : Type u_1} [] (K : ) (x : X) :
K.shiftr.find x = K.find x + 1
theorem CompactExhaustion.mem_diff_shiftr_find {X : Type u_1} [] (K : ) (x : X) :
x K.shiftr (K.find x + 1) \ K.shiftr (K.find 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.instInhabitedOfLocallyCompactSpace {X : Type u_1} [] :
Equations
• CompactExhaustion.instInhabitedOfLocallyCompactSpace = { default := }