Locally compact spaces #
We define the following classes of topological spaces:
We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.
Every point of a weakly locally compact space admits a compact neighborhood.
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
C(X, Y) is given the compact-open topology.
WeaklyLocallyCompactSpace, a typeclass that only assumes
that each point has a compact neighborhood.
In a locally compact space, every neighbourhood of every point contains a compact neighbourhood of that same point.
In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use.
For spaces that are not Hausdorff.
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.
In a locally compact space, for every containment
K ⊆ U of a compact set
K in an open
U, there is a compact neighborhood
L such that
K ⊆ L ⊆ U: equivalently, there is a
L such that
K ⊆ interior L and
L ⊆ U.
exists_compact_closed_between, in which one guarantees additionally that
L is closed
if the space is regular.