# Documentation

Mathlib.Topology.Compactness.LocallyCompact

# Locally compact spaces #

We define the following classes of topological spaces:

• WeaklyLocallyCompactSpace: every point x has a compact neighborhood.
• LocallyCompactSpace: for every point x, every open neighborhood of x contains a compact neighborhood of x. The definition is formulated in terms of the neighborhood filter.
class WeaklyLocallyCompactSpace (X : Type u_4) [] :

We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.

• exists_compact_mem_nhds : ∀ (x : X), ∃ (s : Set X), s nhds x

Every point of a weakly locally compact space admits a compact neighborhood.

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

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

theorem disjoint_nhds_cocompact {X : Type u_1} [] (x : X) :
Disjoint (nhds x) ()

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

class LocallyCompactSpace (X : Type u_4) [] :

There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed for the evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the compact-open topology.

See also WeaklyLocallyCompactSpace, a typeclass that only assumes that each point has a compact neighborhood.

• local_compact_nhds : ∀ (x : X), nnhds x, ∃ s ∈ nhds x, s n

In a locally compact space, every neighbourhood of every point contains a compact neighbourhood of that same point.

Instances
theorem compact_basis_nhds {X : Type u_1} [] (x : X) :
Filter.HasBasis (nhds x) (fun (s : Set X) => s nhds x ) fun (s : Set X) => s
theorem local_compact_nhds {X : Type u_1} [] {x : X} {n : Set X} (h : n nhds x) :
∃ s ∈ nhds x, s n
theorem locallyCompactSpace_of_hasBasis {X : Type u_1} [] {ι : 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)) :
instance Prod.locallyCompactSpace (X : Type u_4) (Y : Type u_5) [] [] :
Equations
instance Pi.locallyCompactSpace_of_finite {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LocallyCompactSpace (X i)] [] :
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
instance Function.locallyCompactSpace_of_finite {Y : Type u_2} {ι : Type u_3} [] [] :
Equations
instance Function.locallyCompactSpace {Y : Type u_2} {ι : Type u_3} [] [] :
Equations
theorem exists_compact_subset {X : Type u_1} [] {x : X} {U : Set X} (hU : ) (hx : x U) :
∃ (K : Set X), x 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.

instance instWeaklyLocallyCompactSpace_1 {X : Type u_1} [] :
Equations
• (_ : ) = (_ : )
theorem exists_compact_between {X : Type u_1} [] [hX : ] {K : Set X} {U : Set X} (hK : ) (hU : ) (h_KU : K U) :
∃ (L : Set X), K 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.

theorem ClosedEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsClosed.locallyCompactSpace {X : Type u_1} [] {s : Set X} (hs : ) :
theorem OpenEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem IsOpen.locallyCompactSpace {X : Type u_1} [] {s : Set X} (hs : ) :