hasBasis_opens_closure — Mathlib

English

The neighborhood basis can be taken from closures of open sets containing the point.

Русский

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

LaTeX

$$$\forall x:\, (\mathcal N x).HasBasis (\lambda s. x \in s \land IsOpen(s)) closure$$$

Lean4

theorem hasBasis_opens_closure (x : X) : (𝓝 x).HasBasis (fun s => x ∈ s ∧ IsOpen s) closure :=
  (nhds_basis_opens x).nhds_closure

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