isGδ — Mathlib

English

Any finite subset of a space with FirstCountable topology is a Gδ set.

Русский

Любое конечное подмножество пространства с топологией первого счетности является множеством Gδ.

LaTeX

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

Lean4

theorem isGδ [FirstCountableTopology X] {s : Set X} [T1Space X] (hs : s.Finite) : IsGδ s :=
  Finite.induction_on _ hs .empty fun _ _ ↦ .union (.singleton _)

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