Theorems · Theorem · general topology

compact_basis_nhds

∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] (x : X),
  (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsCompact s) fun s => s

Defined in

Mathlib.Topology.Compactness.LocallyCompact

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyCompactSpace