compact_basis_nhds — Mathlib

English

For a locally compact space, the neighborhood filter at x has a basis consisting of compact sets.

Русский

Для локально компактного пространства множества окрестностей точки x имеют базис, состоящий из компактных множеств.

LaTeX

$$$\forall X\,[TopologicalSpace\;X]\,[LocallyCompactSpace\;X]\ (x:X), (\nhds\;x).HasBasis (fun s=> s\in(\nhds\;x)\wedge IsCompact\;s) (fun s=> s)$$$

Lean4

theorem compact_basis_nhds [LocallyCompactSpace X] (x : X) :
    (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsCompact s) fun s => s :=
  hasBasis_self.2 <| by simpa only [and_comm] using LocallyCompactSpace.local_compact_nhds x

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