singleton — Mathlib

English

A singleton {x} is a Gδ set in any First-Countable T1 space.

Русский

Одиночка {x} является множеством Gδ в любом пространстве с первой счетностью и T1.

LaTeX

$$$\\operatorname{IsGδ}(\\{x\\})$$$

Lean4

protected theorem singleton [FirstCountableTopology X] [T1Space X] (x : X) : IsGδ ({ x } : Set X) :=
  by
  rcases (nhds_basis_opens x).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
  rw [← biInter_basis_nhds h_basis.toHasBasis]
  exact .biInter (to_countable _) fun n _ => (hU n).2.isGδ

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