basis_nhds — Mathlib

English

The neighborhood filter at x has a basis consisting of all open neighborhoods of x.

Русский

Фильтр окрестностей x имеет базис, состоящий из всех открытых окрестностей x.

LaTeX

$$$(\\\\mathcal{N}(x)) \\\\text{ has basis } \\\\{ U : OpenNhdsOf(x) \\\\}$.$$

Lean4

theorem basis_nhds : (𝓝 x).HasBasis (fun _ : OpenNhdsOf x => True) (↑) :=
  (nhds_basis_opens x).to_hasBasis (fun U hU => ⟨⟨⟨U, hU.2⟩, hU.1⟩, trivial, Subset.rfl⟩) fun U _ =>
    ⟨U, ⟨⟨U.mem, U.isOpen⟩, Subset.rfl⟩⟩

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