isGδ_compl

Mathlib.Topology.Separation.GDelta

URI: https://scilib.ai/kg/mathlib#Set.Finite.isGδ_compl

English

If s is a finite subset of a T1 space X, then its complement s^c is a Gδ set.

Русский

Если s — конечное подмножество X в пространстве T1, то its complement X \\ s — множество Gδ.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru