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} [TopologicalSpace X] (s : Set X) : Prop

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

Equations

• IsSigmaCompact s = ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = s

theorem IsCompact.isSigmaCompact {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) : IsSigmaCompact s

Compact sets are σ-compact.

@[simp]

theorem isSigmaCompact_empty {X : Type u_1} [TopologicalSpace X] : IsSigmaCompact ∅

The empty set is σ-compact.

theorem isSigmaCompact_iUnion_of_isCompact {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [hι : Countable ι] (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} [TopologicalSpace X] {S : Set (Set X)} (hc : S.Countable) (hcomp : ∀ s ∈ S, IsCompact s) : IsSigmaCompact (⋃₀ S)

Countable unions of compact sets are σ-compact.

theorem isSigmaCompact_iUnion {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [Countable ι] (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} [TopologicalSpace X] (S : Set (Set X)) (hc : S.Countable) (hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s) : IsSigmaCompact (⋃₀ S)

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

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

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

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

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

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

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {s : Set X} (hs : IsSigmaCompact s) : IsSigmaCompact (f '' s)

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

theorem IsInducing.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsInducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

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

@[deprecated IsInducing.isSigmaCompact_iff]

theorem Inducing.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsInducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Alias of IsInducing.isSigmaCompact_iff.

---

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

theorem IsEmbedding.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsEmbedding f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

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

@[deprecated IsEmbedding.isSigmaCompact_iff]

theorem Embedding.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (hf : IsEmbedding f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Alias of IsEmbedding.isSigmaCompact_iff.

---

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} [TopologicalSpace X] {p : X → Prop} {s : Set { a : X // p a }} : IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' s)

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

class SigmaCompactSpace (X : Type u_4) [TopologicalSpace X] : Prop

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.

theorem SigmaCompactSpace.isSigmaCompact_univ {X : Type u_4} : ∀ {inst : TopologicalSpace X} [self : SigmaCompactSpace X], IsSigmaCompact Set.univ

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

theorem isSigmaCompact_univ_iff {X : Type u_1} [TopologicalSpace X] : IsSigmaCompact Set.univ ↔ SigmaCompactSpace X

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

theorem isSigmaCompact_univ {X : Type u_1} [TopologicalSpace X] [h : SigmaCompactSpace X] : IsSigmaCompact Set.univ

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

theorem SigmaCompactSpace_iff_exists_compact_covering {X : Type u_1} [TopologicalSpace X] : SigmaCompactSpace X ↔ ∃ (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} [TopologicalSpace X] [h : SigmaCompactSpace X] : ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = Set.univ

theorem isSigmaCompact_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) [SigmaCompactSpace X] : IsSigmaCompact (Set.range f)

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

theorem isSigmaCompact_iff_isSigmaCompact_univ {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsSigmaCompact s ↔ IsSigmaCompact Set.univ

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

theorem isSigmaCompact_iff_sigmaCompactSpace {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsSigmaCompact s ↔ SigmaCompactSpace ↑s

@[instance 200]

instance CompactSpace.sigma_compact {X : Type u_1} [TopologicalSpace X] [CompactSpace X] : SigmaCompactSpace X

Equations

• ⋯ = ⋯

theorem SigmaCompactSpace.of_countable {X : Type u_1} [TopologicalSpace X] (S : Set (Set X)) (Hc : S.Countable) (Hcomp : ∀ s ∈ S, IsCompact s) (HU : ⋃₀ S = Set.univ) : SigmaCompactSpace X

@[instance 100]

instance sigmaCompactSpace_of_locally_compact_second_countable {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [SecondCountableTopology X] : SigmaCompactSpace X

Equations

• ⋯ = ⋯

def compactCovering (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] : ℕ → Set X

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

Equations

• compactCovering X = Set.Accumulate ⋯.choose

theorem isCompact_compactCovering (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] (n : ℕ) : IsCompact (compactCovering X n)

theorem iUnion_compactCovering (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] : ⋃ (n : ℕ), compactCovering X n = Set.univ

theorem iUnion_closure_compactCovering (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] : ⋃ (n : ℕ), closure (compactCovering X n) = Set.univ

theorem compactCovering_subset (X : Type u_1) [TopologicalSpace X] [SigmaCompactSpace X] ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m ≤ n) : compactCovering X m ⊆ compactCovering X n

theorem exists_mem_compactCovering {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] (x : X) : ∃ (n : ℕ), x ∈ compactCovering X n

instance instSigmaCompactSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] [SigmaCompactSpace Y] : SigmaCompactSpace (X × Y)

Equations

• ⋯ = ⋯

instance instSigmaCompactSpaceForallOfFinite {ι : Type u_3} [Finite ι] {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} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] [SigmaCompactSpace Y] : SigmaCompactSpace (X ⊕ Y)

Equations

• ⋯ = ⋯

instance instSigmaCompactSpaceSigmaOfCountable {ι : Type u_3} [Countable ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] : SigmaCompactSpace ((i : ι) × X i)

Equations

• ⋯ = ⋯

theorem IsClosedEmbedding.sigmaCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] {e : Y → X} (he : IsClosedEmbedding e) : SigmaCompactSpace Y

@[deprecated IsClosedEmbedding.sigmaCompactSpace]

theorem ClosedEmbedding.sigmaCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] {e : Y → X} (he : IsClosedEmbedding e) : SigmaCompactSpace Y

Alias of IsClosedEmbedding.sigmaCompactSpace.

theorem IsClosed.sigmaCompactSpace {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {s : Set X} (hs : IsClosed s) : SigmaCompactSpace ↑s

instance instSigmaCompactSpaceULift {Y : Type u_2} [TopologicalSpace Y] [SigmaCompactSpace Y] : SigmaCompactSpace (ULift.{u, u_2} Y)

Equations

• ⋯ = ⋯

theorem LocallyFinite.countable_univ {X : Type u_1} {ι : Type u_3} [TopologicalSpace X] [SigmaCompactSpace X] {f : ι → Set X} (hf : LocallyFinite f) (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} [TopologicalSpace X] [SigmaCompactSpace X] {ι : Type u_4} {f : ι → Set X} (hf : LocallyFinite f) (hne : ∀ (i : ι), (f i).Nonempty) : Encodable ι

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

Equations

• hf.encodable hne = Encodable.ofEquiv (↑Set.univ) (Equiv.Set.univ ι).symm

theorem countable_cover_nhdsWithin_of_sigma_compact {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X} {s : Set X} (hs : IsClosed s) (hf : ∀ x ∈ s, f x ∈ nhdsWithin x s) : ∃ t ⊆ s, t.Countable ∧ 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} [TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X} (hf : ∀ (x : X), f x ∈ nhds x) : ∃ (s : Set X), s.Countable ∧ ⋃ 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) [TopologicalSpace X] : 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.

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

The sets in the compact exhaustion are in fact compact.

theorem CompactExhaustion.subset_interior_succ' {X : Type u_4} [TopologicalSpace X] (self : CompactExhaustion X) (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} [TopologicalSpace X] (self : CompactExhaustion X) : ⋃ (n : ℕ), self.toFun n = Set.univ

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

instance CompactExhaustion.instFunLikeNatSet {X : Type u_1} [TopologicalSpace X] : FunLike (CompactExhaustion X) ℕ (Set X)

Equations

• CompactExhaustion.instFunLikeNatSet = { coe := CompactExhaustion.toFun, coe_injective' := ⋯ }

instance CompactExhaustion.instRelHomClassNatSetLeSubset {X : Type u_1} [TopologicalSpace X] : RelHomClass (CompactExhaustion X) LE.le Subset

Equations

• ⋯ = ⋯

@[simp]

theorem CompactExhaustion.toFun_eq_coe {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) : K.toFun = ⇑K

theorem CompactExhaustion.isCompact {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ) : IsCompact (K n)

theorem CompactExhaustion.subset_interior_succ {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ) : K n ⊆ interior (K (n + 1))

theorem CompactExhaustion.subset {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m ≤ n) : K m ⊆ K n

theorem CompactExhaustion.subset_succ {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (n : ℕ) : K n ⊆ K (n + 1)

theorem CompactExhaustion.subset_interior {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) ⦃m : ℕ⦄ ⦃n : ℕ⦄ (h : m < n) : K m ⊆ interior (K n)

theorem CompactExhaustion.iUnion_eq {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) : ⋃ (n : ℕ), K n = Set.univ

theorem CompactExhaustion.exists_mem {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) : ∃ (n : ℕ), x ∈ K n

theorem CompactExhaustion.exists_superset_of_isCompact {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {s : Set X} (hs : IsCompact s) : ∃ (n : ℕ), s ⊆ K n

A compact exhaustion eventually covers any compact set.

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

The minimal n such that x ∈ K n.

Equations

• K.find x = Nat.find ⋯

theorem CompactExhaustion.mem_find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) : x ∈ K (K.find x)

theorem CompactExhaustion.mem_iff_find_le {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {x : X} {n : ℕ} : x ∈ K n ↔ K.find x ≤ n

def CompactExhaustion.shiftr {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) : CompactExhaustion X

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' := ⋯ }

@[simp]

theorem CompactExhaustion.find_shiftr {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) : K.shiftr.find x = K.find x + 1

theorem CompactExhaustion.mem_diff_shiftr_find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) : x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x)

noncomputable def CompactExhaustion.choice (X : Type u_4) [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [SigmaCompactSpace X] : CompactExhaustion X

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

Equations

• CompactExhaustion.choice X = Classical.choice ⋯

noncomputable instance CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfLocallyCompactSpace {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] [LocallyCompactSpace X] : Inhabited (CompactExhaustion X)

Equations

• CompactExhaustion.instInhabitedOfSigmaCompactSpaceOfLocallyCompactSpace = { default := CompactExhaustion.choice X }