# Locally compact spaces #

This file contains basic results about locally compact spaces.

source
instance instWeaklyLocallyCompactSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [WeaklyLocallyCompactSpace Y] :
WeaklyLocallyCompactSpace (X × Y)
source
instance instWeaklyLocallyCompactSpaceForallOfFinite {ι : Type u_4} [Finite ι] {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), WeaklyLocallyCompactSpace (X i)] :
WeaklyLocallyCompactSpace ((i : ι) → X i)
source
@[instance 100]
instance instWeaklyLocallyCompactSpaceOfCompactSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] :
WeaklyLocallyCompactSpace X
source
theorem Topology.IsClosedEmbedding.weaklyLocallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
WeaklyLocallyCompactSpace X
source
theorem IsClosed.weaklyLocallyCompactSpace {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] {s : Set X} (hs : IsClosed s) :
WeaklyLocallyCompactSpace ↑s
source
theorem IsOpenQuotientMap.weaklyLocallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] {f : X → Y} (hf : IsOpenQuotientMap f) :
WeaklyLocallyCompactSpace Y
source
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.

source
theorem disjoint_nhds_cocompact {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] (x : X) :
Disjoint (nhds x) (Filter.cocompact X)

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

source
theorem compact_basis_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsCompact s) fun (s : Set X) => s
source
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
source
theorem LocallyCompactSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : X → Type u_4} {p : (x : X) → ι x → Prop} {s : (x : X) → ι x → Set X} (h : ∀ (x : X), (nhds x).HasBasis (p x) (s x)) (hc : ∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) :
LocallyCompactSpace X
source
instance Prod.locallyCompactSpace (X : Type u_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X] [LocallyCompactSpace Y] :
LocallyCompactSpace (X × Y)
source
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.

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

source
instance Function.locallyCompactSpace_of_finite {Y : Type u_2} {ι : Type u_3} [TopologicalSpace Y] [Finite ι] [LocallyCompactSpace Y] :
LocallyCompactSpace (ι → Y)
source
instance Function.locallyCompactSpace {Y : Type u_2} {ι : Type u_3} [TopologicalSpace Y] [LocallyCompactSpace Y] [CompactSpace Y] :
LocallyCompactSpace (ι → Y)
source
@[instance 900]
instance instLocallyCompactPairOfLocallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X] :
LocallyCompactPair X Y
source
@[instance 100]
instance instWeaklyLocallyCompactSpaceOfLocallyCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] :
WeaklyLocallyCompactSpace X
source
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.

source
theorem exists_mem_nhdsSet_isCompact_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactPair X Y] {f : X → Y} {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`.

source
theorem exists_compact_between {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {K 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.

source
theorem IsOpenQuotientMap.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X] {f : X → Y} (hf : IsOpenQuotientMap f) :
LocallyCompactSpace Y
source
theorem Topology.IsInducing.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : IsInducing f) (h : IsLocallyClosed (Set.range f)) :
LocallyCompactSpace X

If `f` is a topology inducing map with a locally compact codomain and a locally closed range, then the domain of `f` is a locally compact space.

source
theorem Topology.IsClosedEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
LocallyCompactSpace X
source
theorem Topology.IsOpenEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : IsOpenEmbedding f) :
LocallyCompactSpace X
source
theorem IsLocallyClosed.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {s : Set X} (hs : IsLocallyClosed s) :
LocallyCompactSpace ↑s
source
theorem IsClosed.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {s : Set X} (hs : IsClosed s) :
LocallyCompactSpace ↑s
source
theorem IsOpen.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {s : Set X} (hs : IsOpen s) :
LocallyCompactSpace ↑s