Commit 2024-06-26 01:20 d9d3a89b

chore: reverse gdelta/separation dependency (#13694) This reversal will allow for the following definition for a perfectly normal space (with $T_1$ this is T_6, the last "whole number" separation axiom missing from mathlib), proposed at #13517.

/-- A topological space `X` is a *perfectly normal space* provided it is normal and
closed sets are Gδ. -/
class PerfectlyNormalSpace (X : Type u) [TopologicalSpace X] extends NormalSpace X : Prop where
    closed_gdelta : ∀ ⦃h : Set X⦄, IsClosed h → IsGδ h