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

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), IsCompact s ∧ s ∈ nhds x

  Every point of a weakly locally compact 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

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

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

Equations

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

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

Equations

• (_ : WeaklyLocallyCompactSpace X) = (_ : WeaklyLocallyCompactSpace X)

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.

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

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), ∀ n ∈ nhds x, ∃ 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.

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] {ι : 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

@[deprecated LocallyCompactSpace.of_hasBasis]

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

Alias of LocallyCompactSpace.of_hasBasis.

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

Equations

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

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

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

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

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

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

Equations

• (_ : LocallyCompactSpace (ι → Y)) = (_ : LocallyCompactSpace (ι → Y))

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

Equations

• (_ : LocallyCompactSpace (ι → Y)) = (_ : LocallyCompactSpace (ι → Y))

class LocallyCompactPair (X : Type u_4) (Y : Type u_5) [TopologicalSpace X] [TopologicalSpace Y] : Prop

We say that X and Y are a locally compact pair of topological spaces, if for any continuous map f : X → Y, a point x : X, and a neighbourhood s ∈ 𝓝 (f x), there exists a compact neighbourhood K ∈ 𝓝 x such that f maps K to s.

This is a technical assumption that appears in several theorems, most notably in ContinuousMap.continuous_comp' and ContinuousMap.continuous_eval. It is satisfied in two cases:

• if X is a locally compact topological space, for obvious reasons;
• if X is a weakly locally compact topological space and Y is a Hausdorff space; this fact is a simple generalization of the theorem saying that a weakly locally compact Hausdorff topological space is locally compact.

• exists_mem_nhds_isCompact_mapsTo : ∀ {f : X → Y} {x : X} {s : Set Y}, Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s

  If f : X → Y is a continuous map in a locally compact pair of topological spaces and s : Set Y is a neighbourhood of f x, x : X, then there exists a compact neighbourhood K of x such that f maps K to s.

instance instLocallyCompactPair {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [LocallyCompactSpace X] : LocallyCompactPair X Y

Equations

• (_ : LocallyCompactPair X Y) = (_ : LocallyCompactPair X Y)

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

Equations

• (_ : WeaklyLocallyCompactSpace X) = (_ : WeaklyLocallyCompactSpace X)

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

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.

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