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 {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

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

Equations

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

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

Compact sets are σ-compact.

@[simp]

theorem isSigmaCompact_empty {α : Type u} [TopologicalSpace α] : IsSigmaCompact ∅

The empty set is σ-compact.

theorem isSigmaCompact_iUnion_of_isCompact {α : Type u} [TopologicalSpace α] {ι : Type u_3} [hι : Countable ι] (s : ι → Set α) (hcomp : ∀ (i : ι), IsCompact (s i)) : IsSigmaCompact (⋃ i, s i)

Countable unions of compact sets are σ-compact.

theorem isSigmaCompact_sUnion_of_isCompact {α : Type u} [TopologicalSpace α] {S : Set (Set α)} (hc : Set.Countable S) (hcomp : ∀ (s : Set α), s ∈ S → IsCompact s) : IsSigmaCompact (⋃₀ S)

Countable unions of compact sets are σ-compact.

theorem isSigmaCompact_iUnion {α : Type u} [TopologicalSpace α] {ι : Type u_3} [Countable ι] (s : ι → Set α) (hcomp : ∀ (i : ι), IsSigmaCompact (s i)) : IsSigmaCompact (⋃ i, s i)

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

theorem isSigmaCompact_sUnion {α : Type u} [TopologicalSpace α] (S : Set (Set α)) (hc : Set.Countable S) (hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s) : IsSigmaCompact (⋃₀ S)

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

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

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

theorem IsSigmaCompact.of_isClosed_subset {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) {s : Set α} (hs : IsSigmaCompact s) : IsSigmaCompact (f '' s)

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

theorem Inducing.isSigmaCompact_iff {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : Inducing f) : IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : Embedding 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.

theorem Subtype.isSigmaCompact_iff {α : Type u} [TopologicalSpace α] {p : α → Prop} {s : Set { a // p a }} : IsSigmaCompact s ↔ IsSigmaCompact (Subtype.val '' s)

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

class SigmaCompactSpace (α : Type u_3) [TopologicalSpace α] : Prop

• isSigmaCompact_univ : IsSigmaCompact Set.univ

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

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.

theorem isSigmaCompact_univ_iff {α : Type u} [TopologicalSpace α] : IsSigmaCompact Set.univ ↔ SigmaCompactSpace α

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

theorem isSigmaCompact_univ {α : Type u} [TopologicalSpace α] [h : SigmaCompactSpace α] : IsSigmaCompact Set.univ

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

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

theorem isSigmaCompact_range {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) [SigmaCompactSpace α] : IsSigmaCompact (Set.range f)

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

theorem isSigmaCompact_iff_isSigmaCompact_univ {α : Type u} [TopologicalSpace α] {s : Set α} : IsSigmaCompact s ↔ IsSigmaCompact Set.univ

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

theorem isSigmaCompact_iff_sigmaCompactSpace {α : Type u} [TopologicalSpace α] {s : Set α} : IsSigmaCompact s ↔ SigmaCompactSpace ↑s

instance CompactSpace.sigma_compact {α : Type u} [TopologicalSpace α] [CompactSpace α] : SigmaCompactSpace α

Equations

• @CompactSpace.sigma_compact = @CompactSpace.sigma_compact.proof_1

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

instance sigmaCompactSpace_of_locally_compact_second_countable {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [TopologicalSpace.SecondCountableTopology α] : SigmaCompactSpace α

Equations

• @sigmaCompactSpace_of_locally_compact_second_countable = @sigmaCompactSpace_of_locally_compact_second_countable.proof_1

def compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] : ℕ → Set α

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

Equations

• compactCovering α = Set.Accumulate (Exists.choose (_ : ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = Set.univ))

theorem isCompact_compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] (n : ℕ) : IsCompact (compactCovering α n)

theorem iUnion_compactCovering (α : Type u) [TopologicalSpace α] [SigmaCompactSpace α] : ⋃ n, compactCovering α n = Set.univ

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

theorem exists_mem_compactCovering {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] (x : α) : ∃ n, x ∈ compactCovering α n

instance instSigmaCompactSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] [SigmaCompactSpace β] : SigmaCompactSpace (α × β)

Equations

• @instSigmaCompactSpaceProdInstTopologicalSpaceProd = @instSigmaCompactSpaceProdInstTopologicalSpaceProd.proof_1

instance instSigmaCompactSpaceForAllTopologicalSpace {ι : Type u_1} {π : ι → Type u_2} [Finite ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] : SigmaCompactSpace ((i : ι) → π i)

Equations

• @instSigmaCompactSpaceForAllTopologicalSpace = @instSigmaCompactSpaceForAllTopologicalSpace.proof_1

instance instSigmaCompactSpaceSumInstTopologicalSpaceSum {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] [SigmaCompactSpace β] : SigmaCompactSpace (α ⊕ β)

Equations

• @instSigmaCompactSpaceSumInstTopologicalSpaceSum = @instSigmaCompactSpaceSumInstTopologicalSpaceSum.proof_1

instance instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {π : ι → Type u_2} [Countable ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), SigmaCompactSpace (π i)] : SigmaCompactSpace ((i : ι) × π i)

Equations

• @instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma = @instSigmaCompactSpaceSigmaInstTopologicalSpaceSigma.proof_1

theorem ClosedEmbedding.sigmaCompactSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [SigmaCompactSpace α] {e : β → α} (he : ClosedEmbedding e) : SigmaCompactSpace β

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

instance instSigmaCompactSpaceULiftTopologicalSpace {β : Type v} [TopologicalSpace β] [SigmaCompactSpace β] : SigmaCompactSpace (ULift.{u, v} β)

Equations

• @instSigmaCompactSpaceULiftTopologicalSpace = @instSigmaCompactSpaceULiftTopologicalSpace.proof_1

theorem LocallyFinite.countable_univ {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {ι : Type u_3} {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Set.Countable Set.univ

If α is a σ-compact space, then a locally finite family of nonempty sets of α can have only countably many elements, Set.Countable version.

noncomputable def LocallyFinite.encodable {α : Type u} [TopologicalSpace α] [SigmaCompactSpace α] {ι : Type u_3} {f : ι → Set α} (hf : LocallyFinite f) (hne : ∀ (i : ι), Set.Nonempty (f i)) : Encodable ι

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

Equations

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

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

• toFun : ℕ → Set X

  The sequence of compact sets that form a compact exhaustion.

• isCompact' : ∀ (n : ℕ), IsCompact (CompactExhaustion.toFun s n)

  The sets in the compact exhaustion are in fact compact.

• subset_interior_succ' : ∀ (n : ℕ), CompactExhaustion.toFun s 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, CompactExhaustion.toFun s n = Set.univ

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

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

instance CompactExhaustion.instRelHomClassCompactExhaustionNatSetLeInstLENatSubsetInstHasSubsetSet {α : Type u} [TopologicalSpace α] : RelHomClass (CompactExhaustion α) LE.le Subset

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompactExhaustion.toFun_eq_coe {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : K.toFun = ↑K

theorem CompactExhaustion.isCompact {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (n : ℕ) : IsCompact (↑K n)

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

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

theorem CompactExhaustion.subset_succ {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (n : ℕ) : ↑K n ⊆ ↑K (n + 1)

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

theorem CompactExhaustion.iUnion_eq {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : ⋃ n, ↑K n = Set.univ

theorem CompactExhaustion.exists_mem {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : ∃ n, x ∈ ↑K n

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

The minimal n such that x ∈ K n.

Equations

• CompactExhaustion.find K x = Nat.find (_ : ∃ n, x ∈ ↑K n)

theorem CompactExhaustion.mem_find {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) (x : α) : x ∈ ↑K (CompactExhaustion.find K x)

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

def CompactExhaustion.shiftr {α : Type u} [TopologicalSpace α] (K : CompactExhaustion α) : CompactExhaustion α

Prepend the empty set to a compact exhaustion K n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

noncomputable def CompactExhaustion.choice (X : Type u_3) [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 (_ : Nonempty (CompactExhaustion X))

noncomputable instance CompactExhaustion.instInhabitedCompactExhaustion {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [SigmaCompactSpace α] : Inhabited (CompactExhaustion α)

Equations

• CompactExhaustion.instInhabitedCompactExhaustion = { default := CompactExhaustion.choice α }