disjoint_nhds_cocompact — Mathlib

English

In a weakly locally compact space, the neighborhood filter at x and the cocompact filter are disjoint.

Русский

В слабой локально компактной пространстве фильтр соседств по точке x и фильтр кокомпактности не пересекаются.

LaTeX

$$$\forall X\,[TopologicalSpace\;X]\,[WeaklyLocallyCompactSpace\;X]\ (x:X),\ Disjoint\ (\nhds\;x)\ (cocompact\;X)$$$

Lean4

/-- In a weakly locally compact space,
the filters `𝓝 x` and `cocompact X` are disjoint for all `X`. -/
theorem disjoint_nhds_cocompact [WeaklyLocallyCompactSpace X] (x : X) : Disjoint (𝓝 x) (cocompact X) :=
  let ⟨_, hc, hx⟩ := exists_compact_mem_nhds x
  disjoint_of_disjoint_of_mem disjoint_compl_right hx hc.compl_mem_cocompact

Похожие утверждения