Documentation

Mathlib.Topology.Compactness.LocallyCompact

Locally compact spaces #

We define the following classes of topological spaces:

instance instWeaklyLocallyCompactSpaceForAllTopologicalSpace {ι : Type u_4} [Finite ι] {X : ιType u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), WeaklyLocallyCompactSpace (X i)] :
WeaklyLocallyCompactSpace ((i : ι) → X i)
Equations
  • =
theorem exists_compact_superset {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) :
∃ (K' : Set X), IsCompact K' K interior K'

In a weakly locally compact space, every compact set is contained in the interior of a compact set.

In a weakly locally compact space, the filters 𝓝 x and cocompact X are disjoint for all X.

theorem compact_basis_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] (x : X) :
Filter.HasBasis (nhds x) (fun (s : Set X) => s nhds x IsCompact s) fun (s : Set X) => s
theorem local_compact_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {n : Set X} (h : n nhds x) :
∃ s ∈ nhds x, s n IsCompact s
theorem LocallyCompactSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : XType u_4} {p : (x : X) → ι xProp} {s : (x : X) → ι xSet X} (h : ∀ (x : X), Filter.HasBasis (nhds x) (p x) (s x)) (hc : ∀ (x : X) (i : ι x), p x iIsCompact (s x i)) :
@[deprecated LocallyCompactSpace.of_hasBasis]
theorem locallyCompactSpace_of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : XType u_4} {p : (x : X) → ι xProp} {s : (x : X) → ι xSet X} (h : ∀ (x : X), Filter.HasBasis (nhds x) (p x) (s x)) (hc : ∀ (x : X) (i : ι x), p x iIsCompact (s x i)) :

Alias of LocallyCompactSpace.of_hasBasis.

instance Pi.locallyCompactSpace_of_finite {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyCompactSpace (X i)] [Finite ι] :
LocallyCompactSpace ((i : ι) → X i)

In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use.

Equations
  • =
instance Pi.locallyCompactSpace {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyCompactSpace (X i)] [∀ (i : ι), CompactSpace (X i)] :
LocallyCompactSpace ((i : ι) → X i)

For spaces that are not Hausdorff.

Equations
  • =
Equations
  • =
Equations
  • =
theorem exists_compact_subset {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x U) :
∃ (K : Set X), IsCompact K x interior K K U

A reformulation of the definition of locally compact space: In a locally compact space, every open set containing x has a compact subset containing x in its interior.

theorem exists_mem_nhdsSet_isCompact_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] {f : XY} {K : Set X} {U : Set Y} (hf : Continuous f) (hK : IsCompact K) (hU : IsOpen U) (hKU : Set.MapsTo f K U) :
∃ L ∈ nhdsSet K, IsCompact L Set.MapsTo f L U

If f : X → Y is a continuous map in a locally compact pair of topological spaces, K : set X is a compact set, and U is an open neighbourhood of f '' K, then there exists a compact neighbourhood L of K such that f maps L to U.

This is a generalization of exists_mem_nhds_isCompact_mapsTo.

theorem exists_compact_between {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {K : Set X} {U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K U) :
∃ (L : Set X), IsCompact L K interior L L U

In a locally compact space, for every containment K ⊆ U of a compact set K in an open set U, there is a compact neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact L such that K ⊆ interior L and L ⊆ U. See also exists_compact_closed_between, in which one guarantees additionally that L is closed if the space is regular.