Theorems · Theorem · general topology

IsCompact.nhdsSet_basis_isCompact

∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {K : Set X},
  IsCompact K → (nhdsSet K).HasBasis (fun L => L ∈ nhdsSet K ∧ IsCompact L) id

In a (possibly non-Hausdorff) locally compact space, for every compact set K, 𝓝ˢ K has a basis consisting of compact sets.

Defined in

Mathlib.Topology.Compactness.LocallyCompact

Cited by

8 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLocallyCompactSpace