Theorems · Theorem · general topology

IsCompact.nhdsSet_basis_isCompact_isClosed

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

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

Defined in

Mathlib.Topology.Separation.Regular

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyCompactSpaceRegularSpace