nhds_basis_closeds — Mathlib

English

The neighborhoods of x have a basis given by complements of closed sets not containing x.

Русский

Окрестности x имеют базу, состоящую из комплементов замкнутых множеств, не содержащих x.

LaTeX

$$$(\\mathcal N(x)) \\text{ has basis }\\{\,s^{c} : s \\text{ closed}, x \\notin s\,\\}$$$

Lean4

theorem nhds_basis_closeds (x : X) : (𝓝 x).HasBasis (fun s : Set X => x ∉ s ∧ IsClosed s) compl :=
  ⟨fun t =>
    (nhds_basis_opens x).mem_iff.trans <|
      compl_surjective.exists.trans <| by simp only [isOpen_compl_iff, mem_compl_iff]⟩

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