isGδ — Mathlib

English

In a perfectly normal space, every closed set is a Gδ set.

Русский

В совершенно нормальном пространстве каждая замкнутая подмножество является Gδ.

LaTeX

$$$ \operatorname{IsClosed}(s) \Rightarrow \operatorname{IsG\delta}(s) $$$

Lean4

/-- In a perfectly normal space, all closed sets are Gδ. -/
theorem isGδ [PerfectlyNormalSpace X] {s : Set X} (hs : IsClosed s) : IsGδ s :=
  PerfectlyNormalSpace.closed_gdelta hs

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