Theorems · Theorem · general topology

disjoint_nhds_cocompact

∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] (x : X),
  Disjoint (nhds x) (Filter.cocompact X)

In a weakly locally compact space, the filters 𝓝 x and cocompact X are disjoint for all X.

Defined in

Mathlib.Topology.Compactness.LocallyCompact

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceWeaklyLocallyCompactSpace