Theorems · Theorem · general topology

LocallyCompactSpace.local_compact_nhds

∀ {X : Type u_3} {inst : TopologicalSpace X} [self : LocallyCompactSpace X] (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.

Defined in

Mathlib.Topology.Defs.Filter

Cited by

6 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

LocallyCompactSpace