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δ