Separation properties of topological spaces.

Main definitions

• PerfectlyNormalSpace: A perfectly normal space is a normal space such that closed sets are Gδ.
• T6Space: A T₆ space is a perfectly normal T₀ space. T₆ implies T₅.

Note that mathlib adopts the modern convention that m ≤ n if and only if T_m → T_n, but occasionally the literature swaps definitions for e.g. T₃ and regular.

theorem IsGδ.compl_singleton {X : Type u_1} [TopologicalSpace X] (x : X) [T1Space X] : IsGδ {x}ᶜ

theorem Set.Countable.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Countable) : IsGδ sᶜ

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

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

theorem Finset.isGδ_compl {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) : IsGδ (↑s)ᶜ

theorem IsGδ.singleton {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] [T1Space X] (x : X) : IsGδ {x}

theorem Set.Finite.isGδ {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} [T1Space X] (hs : s.Finite) : IsGδ s

class PerfectlyNormalSpace (X : Type u) [TopologicalSpace X] extends NormalSpace X : Prop

A topological space X is a perfectly normal space provided it is normal and closed sets are Gδ.

• normal (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
• closed_gdelta ⦃h : Set X⦄ : IsClosed h → IsGδ h

theorem Disjoint.hasSeparatingCover_closed_gdelta_right {X : Type u_1} [TopologicalSpace X] {s t : Set X} [NormalSpace X] (st_dis : Disjoint s t) (t_cl : IsClosed t) (t_gd : IsGδ t) : HasSeparatingCover s t

Lemma that allows the easy conclusion that perfectly normal spaces are completely normal.

@[instance 100]

instance PerfectlyNormalSpace.toCompletelyNormalSpace {X : Type u_1} [TopologicalSpace X] [PerfectlyNormalSpace X] : CompletelyNormalSpace X

theorem IsClosed.isGδ {X : Type u_1} [TopologicalSpace X] [PerfectlyNormalSpace X] {s : Set X} (hs : IsClosed s) : IsGδ s

In a perfectly normal space, all closed sets are Gδ.

@[instance 100]

instance instR0SpaceOfPerfectlyNormalSpace {X : Type u_1} [TopologicalSpace X] [PerfectlyNormalSpace X] : R0Space X

theorem Topology.IsInducing.perfectlyNormalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [PerfectlyNormalSpace Y] {e : X → Y} (he : IsInducing e) : PerfectlyNormalSpace X

instance instPerfectlyNormalSpaceElem {X : Type u_1} [TopologicalSpace X] {s : Set X} [PerfectlyNormalSpace X] : PerfectlyNormalSpace ↑s

class T6Space (X : Type u) [TopologicalSpace X] extends T0Space X, PerfectlyNormalSpace X : Prop

A T₆ space is a perfectly normal T₀ space.

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• normal (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
• closed_gdelta ⦃h : Set X⦄ : IsClosed h → IsGδ h

@[instance 100]

instance T6Space.toT5Space {X : Type u_1} [TopologicalSpace X] [T6Space X] : T5Space X

A T₆ space is a T₅ space.

theorem Topology.IsEmbedding.t6Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T6Space Y] {e : X → Y} (he : IsEmbedding e) : T6Space X

instance instT6SpaceElem {X : Type u_1} [TopologicalSpace X] {s : Set X} [T6Space X] : T6Space ↑s