compl_singleton — Mathlib

English

In a T1 topological space, the complement of a singleton is a Gδ set; equivalently, there exists a countable family of open sets whose intersection equals X \ {x}.

Русский

В пространстве топологическом T1 комплемент одиничного множества {x} является множеством Gδ, то есть существует счётное семейство открытых множеств, их пересечение даёт X \\ {x}.

LaTeX

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

Lean4

theorem compl_singleton (x : X) [T1Space X] : IsGδ ({ x }ᶜ : Set X) :=
  isOpen_compl_singleton.isGδ

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