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) [TopologicalSpace X] : Prop

• exists_compact_mem_nhds : ∀ (x : X), ∃ s, IsCompact s ∧ s ∈ nhds x

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

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

instance instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [WeaklyLocallyCompactSpace Y] : WeaklyLocallyCompactSpace (X × Y)

Equations

• @instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd = @instWeaklyLocallyCompactSpaceProdInstTopologicalSpaceProd.proof_1

instance instWeaklyLocallyCompactSpaceForAllTopologicalSpace {ι : Type u_4} [Finite ι] {X : ι → Type u_5} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), WeaklyLocallyCompactSpace (X i)] : WeaklyLocallyCompactSpace ((i : ι) → X i)

Equations

• @instWeaklyLocallyCompactSpaceForAllTopologicalSpace = @instWeaklyLocallyCompactSpaceForAllTopologicalSpace.proof_1

instance instWeaklyLocallyCompactSpace {X : Type u_1} [TopologicalSpace X] [CompactSpace X] : WeaklyLocallyCompactSpace X

Equations

• @instWeaklyLocallyCompactSpace = @instWeaklyLocallyCompactSpace.proof_1

theorem exists_compact_superset {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ K', IsCompact K' ∧ 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} [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.

class LocallyCompactSpace (X : Type u_4) [TopologicalSpace X] : Prop

• local_compact_nhds : ∀ (x : X) (n : Set X), n ∈ nhds x → ∃ s, s ∈ nhds x ∧ s ⊆ n ∧ IsCompact s

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

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.

theorem compact_basis_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] (x : X) : Filter.HasBasis (nhds x) (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s

theorem local_compact_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {n : Set X} (h : n ∈ nhds x) : ∃ s, s ∈ nhds x ∧ s ⊆ n ∧ IsCompact s

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), Filter.HasBasis (nhds x) (p x) (s x)) (hc : ∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) : LocallyCompactSpace X

instance Prod.locallyCompactSpace (X : Type u_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X] [LocallyCompactSpace Y] : LocallyCompactSpace (X × Y)

Equations

• Prod.locallyCompactSpace = Prod.locallyCompactSpace.proof_1

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

• @Pi.locallyCompactSpace_of_finite = @Pi.locallyCompactSpace_of_finite.proof_1

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

• @Pi.locallyCompactSpace = @Pi.locallyCompactSpace.proof_1

instance Function.locallyCompactSpace_of_finite {Y : Type u_2} {ι : Type u_3} [TopologicalSpace Y] [Finite ι] [LocallyCompactSpace Y] : LocallyCompactSpace (ι → Y)

Equations

• @Function.locallyCompactSpace_of_finite = @Function.locallyCompactSpace_of_finite.proof_1

instance Function.locallyCompactSpace {Y : Type u_2} {ι : Type u_3} [TopologicalSpace Y] [LocallyCompactSpace Y] [CompactSpace Y] : LocallyCompactSpace (ι → Y)

Equations

• @Function.locallyCompactSpace = @Function.locallyCompactSpace.proof_1

theorem exists_compact_subset {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {x : X} {U : Set X} (hU : IsOpen U) (hx : x ∈ U) : ∃ K, 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.

instance instWeaklyLocallyCompactSpace_1 {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] : WeaklyLocallyCompactSpace X

Equations

• @instWeaklyLocallyCompactSpace_1 = @instWeaklyLocallyCompactSpace_1.proof_1

theorem exists_compact_between {X : Type u_1} [TopologicalSpace X] [hX : LocallyCompactSpace X] {K : Set X} {U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K ⊆ U) : ∃ L, 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.

theorem ClosedEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : ClosedEmbedding f) : LocallyCompactSpace X

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

theorem OpenEmbedding.locallyCompactSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace Y] {f : X → Y} (hf : OpenEmbedding f) : LocallyCompactSpace X

theorem IsOpen.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] {s : Set X} (hs : IsOpen s) : LocallyCompactSpace ↑s

theorem Ultrafilter.le_nhds_lim {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (F : Ultrafilter X) : ↑F ≤ nhds (Ultrafilter.lim F)