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 : Set.Countable S) (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 : Set.Countable S) (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 : Set.Countable s) (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 Inducing.isSigmaCompact_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (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 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (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 {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 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 CompactSpace.sigma_compact {X : Type u_1} [TopologicalSpace X] [CompactSpace X] : SigmaCompactSpace X

Equations

• (_ : SigmaCompactSpace X) = (_ : SigmaCompactSpace X)

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

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

Equations

• (_ : SigmaCompactSpace X) = (_ : SigmaCompactSpace X)

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 (Exists.choose (_ : ∃ (K : ℕ → Set X), (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ (n : ℕ), K n = Set.univ))

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 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 instSigmaCompactSpaceProdInstTopologicalSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] [SigmaCompactSpace Y] : SigmaCompactSpace (X × Y)

Equations

• (_ : SigmaCompactSpace (X × Y)) = (_ : SigmaCompactSpace (X × Y))

instance instSigmaCompactSpaceForAllTopologicalSpace {ι : Type u_3} [Finite ι] {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SigmaCompactSpace (X i)] : SigmaCompactSpace ((i : ι) → X i)

Equations

• (_ : SigmaCompactSpace ((i : ι) → X i)) = (_ : SigmaCompactSpace ((i : ι) → X i))

instance instSigmaCompactSpaceSumInstTopologicalSpaceSum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SigmaCompactSpace X] [SigmaCompactSpace Y] : SigmaCompactSpace (X ⊕ Y)

Equations

• (_ : SigmaCompactSpace (X ⊕ Y)) = (_ : SigmaCompactSpace (X ⊕ Y))

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

Equations

• (_ : SigmaCompactSpace ((i : ι) × X i)) = (_ : SigmaCompactSpace ((i : ι) × X i))

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

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

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

Equations

• (_ : SigmaCompactSpace (ULift.{u, u_2} Y)) = (_ : SigmaCompactSpace (ULift.{u, u_2} Y))

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

• LocallyFinite.encodable hf 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, 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 {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X} (hf : ∀ (x : X), f x ∈ nhds x) : ∃ (s : Set X), 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_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.

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

Equations

• CompactExhaustion.instFunLikeCompactExhaustionNatSet = { coe := CompactExhaustion.toFun, coe_injective' := (_ : ∀ (x x_1 : CompactExhaustion X), x.toFun = x_1.toFun → x = x_1) }

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

Equations

• (_ : RelHomClass (CompactExhaustion X) LE.le Subset) = (_ : RelHomClass (CompactExhaustion X) LE.le Subset)

@[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

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

The minimal n such that x ∈ K n.

Equations

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

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

theorem CompactExhaustion.mem_iff_find_le {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) {x : X} {n : ℕ} : x ∈ K n ↔ CompactExhaustion.find K 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

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

@[simp]

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

theorem CompactExhaustion.mem_diff_shiftr_find {X : Type u_1} [TopologicalSpace X] (K : CompactExhaustion X) (x : X) : x ∈ (CompactExhaustion.shiftr K) (CompactExhaustion.find K x + 1) \ (CompactExhaustion.shiftr K) (CompactExhaustion.find K 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 (_ : Nonempty (CompactExhaustion X))

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

Equations

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