Documentation

Mathlib.Topology.Separation.GDelta

Separation properties of topological spaces. #

Main definitions #

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 #

theorem IsGδ.compl_singleton {X : Type u_1} [TopologicalSpace X] (x : X) [T1Space X] :
@[deprecated IsGδ.compl_singleton]
theorem isGδ_compl_singleton {X : Type u_1} [TopologicalSpace X] (x : X) [T1Space 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) :
theorem Set.Finite.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Finite) :
theorem Set.Subsingleton.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Subsingleton) :
theorem Finset.isGδ_compl {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) :
IsGδ (↑s)
@[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) :

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

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

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

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

      Instances
        @[instance 100]
        instance T6Space.toT5Space {X : Type u_1} [TopologicalSpace X] [T6Space X] :

        A T₆ space is a T₅ space.

        Equations
        • =