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.

TODO

• Use hasSeparatingCovers_iff_separatedNhds to prove that perfectly normal spaces are completely normal.

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

@[deprecated IsGδ.compl_singleton]

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

Alias of IsGδ.compl_singleton.

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}

@[deprecated IsGδ.singleton]

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

Alias of IsGδ.singleton.

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 : 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 PerfectlyNormalSpace.closed_gdelta {X : Type u} : ∀ {inst : TopologicalSpace X} [self : PerfectlyNormalSpace X] ⦃h : Set X⦄, IsClosed h → IsGδ h

theorem Disjoint.hasSeparatingCover_closed_gdelta_right {X : Type u_1} [TopologicalSpace X] {s : Set X} {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

Equations

• ⋯ = ⋯

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

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

@[instance 100]

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

A T₆ space is a T₅ space.

Equations

• ⋯ = ⋯