Theorems · Theorem · general topology

IsCompact.isCompact_isClosed_basis_nhds

∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {x : X} {L : Set X},
  IsCompact L → L ∈ nhds x → (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x

If a point in an R₁ space has a compact neighborhood, then it has a basis of compact closed neighborhoods.

Defined in

Mathlib.Topology.Separation.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceR1Space