isGδ_compl — Mathlib

English

A subsingleton (a set containing at most one point) has a complement that is a Gδ set in a T1 space.

Русский

Подмножество, содержащее не более одного элемента, имеет комплемент, являющийся множеством Gδ в T1-пространстве.

LaTeX

$$$\\operatorname{IsGδ}(X \\setminus s)$, for subsingleton $s$.$$

Lean4

theorem isGδ_compl {s : Set X} [T1Space X] (hs : s.Subsingleton) : IsGδ sᶜ :=
  hs.finite.isGδ_compl

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