hasBasis_nhds_closure — Mathlib

English

If B is a topological basis, then nhds x has a basis consisting of closures of basis elements containing x.

Русский

Если B — топологический базис, тогда окрестности x имеют базис через замыкания элементов базиса, содержащих x.

LaTeX

$$$\forall X,\forall x,\forall B\; (IsTopologicalBasis\ B) \Rightarrow (nhds x).HasBasis(\\lambda s. s \in nhds x \, ) closure$$$

Lean4

theorem hasBasis_nhds_closure (x : X) : (𝓝 x).HasBasis (fun s => s ∈ 𝓝 x) closure :=
  (𝓝 x).basis_sets.nhds_closure

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