Locally compact spaces #
We define the following classes of topological spaces:
WeaklyLocallyCompactSpace
: every pointx
has a compact neighborhood.LocallyCompactSpace
: for every pointx
, every open neighborhood ofx
contains a compact neighborhood ofx
. The definition is formulated in terms of the neighborhood filter.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
In a weakly locally compact space, every compact set is contained in the interior of a compact set.
In a weakly locally compact space,
the filters 𝓝 x
and cocompact X
are disjoint for all X
.
Equations
- ⋯ = ⋯
In general it suffices that all but finitely many of the spaces are compact, but that's not straightforward to state and use.
Equations
- ⋯ = ⋯
For spaces that are not Hausdorff.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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.
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
.
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.
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.