closed_nhds_basis — Mathlib

English

For every x, the neighborhood filter at x has a basis consisting of closed sets containing x.

Русский

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

LaTeX

$$$\forall x:\, (\mathcal N x).HasBasis(\lambda s:\ Set X\, s\in \mathcal N x \land IsClosed(s))\, id$$$

Lean4

theorem closed_nhds_basis (x : X) : (𝓝 x).HasBasis (fun s : Set X => s ∈ 𝓝 x ∧ IsClosed s) id :=
  hasBasis_self.2 fun _ => exists_mem_nhds_isClosed_subset

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