Structures · Topology

LocallyCompactSpace

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.

Defined in

Mathlib.Topology.Defs.Filter

Shape

One type argument · adds local_compact_nhds