Documentation

Mathlib.Topology.Separation.Regular

Regular, normal, T₃, T₄ and T₅ spaces #

This file continues the study of separation properties of topological spaces, focussing on conditions strictly stronger than T₂.

Main definitions #

See Mathlib.Topology.Separation.GDelta for the definitions of PerfectlyNormalSpace and T6Space.

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.

Main results #

Regular spaces #

If the space is also Lindelöf:

T₃ spaces #

References #

A topological space is called a regular space if for any closed set s and a ∉ s, there exist disjoint open sets U ⊇ s and V ∋ a. We formulate this condition in terms of Disjointness of filters 𝓝ˢ s and 𝓝 a.

  • regular {s : Set X} {a : X} : IsClosed sasDisjoint (nhdsSet s) (nhds a)

    If a is a point that does not belong to a closed set s, then a and s admit disjoint neighborhoods.

Instances
    theorem regularSpace_iff (X : Type u) [TopologicalSpace X] :
    RegularSpace X ∀ {s : Set X} {a : X}, IsClosed sasDisjoint (nhdsSet s) (nhds a)
    theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] :
    [RegularSpace X, ∀ (s : Set X), xclosure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) xclosure s, ∀ (x : X), snhds x, tnhds x, IsClosed t t s, ∀ (x : X), (nhds x).lift' closure nhds x, ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE
    theorem RegularSpace.of_lift'_closure_le {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), (nhds x).lift' closure nhds x) :
    theorem RegularSpace.of_lift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), (nhds x).lift' closure = nhds x) :
    theorem RegularSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : XSort u_3} {p : (a : X) → ι aProp} {s : (a : X) → ι aSet X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a iIsClosed (s a i)) :
    theorem RegularSpace.of_exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), snhds x, tnhds x, IsClosed t t s) :
    @[instance 100]

    A weakly locally compact R₁ space is regular.

    theorem disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} :
    Disjoint (nhdsSet s) (nhds x) xclosure s
    theorem disjoint_nhds_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} :
    Disjoint (nhds x) (nhdsSet s) xclosure s
    @[instance 100]
    instance instR1Space {X : Type u_1} [TopologicalSpace X] [RegularSpace X] :

    A regular space is R₁.

    theorem exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} (h : s nhds x) :
    tnhds x, IsClosed t t s
    theorem closed_nhds_basis {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => s nhds x IsClosed s) id
    theorem lift'_nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
    (nhds x).lift' closure = nhds x
    theorem Filter.HasBasis.nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {ι : Sort u_3} {x : X} {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
    (nhds x).HasBasis p fun (i : ι) => closure (s i)
    theorem hasBasis_nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => s nhds x) closure
    theorem hasBasis_opens_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => x s IsOpen s) closure
    theorem IsCompact.exists_isOpen_closure_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : U nhdsSet K) :
    ∃ (V : Set X), IsOpen V K V closure V U
    theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => x s s B) closure
    @[deprecated Topology.IsInducing.regularSpace (since := "2024-10-28")]
    theorem Inducing.regularSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] {f : YX} (hf : Topology.IsInducing f) :

    Alias of Topology.IsInducing.regularSpace.

    theorem regularSpace_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] (f : YX) :
    theorem regularSpace_sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (h : tT, RegularSpace X) :
    theorem regularSpace_iInf {ι : Sort u_3} {X : Type u_4} {t : ιTopologicalSpace X} (h : ∀ (i : ι), RegularSpace X) :
    theorem RegularSpace.inf {X : Type u_3} {t₁ t₂ : TopologicalSpace X} (h₁ : RegularSpace X) (h₂ : RegularSpace X) :
    instance instRegularSpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] :
    RegularSpace ((i : ι) → X i)
    theorem SeparatedNhds.of_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {s t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :

    In a regular space, if a compact set and a closed set are disjoint, then they have disjoint neighborhoods.

    theorem IsClosed.HasSeparatingCover {X : Type u_1} [TopologicalSpace X] {s t : Set X} [LindelofSpace X] [RegularSpace X] (s_cl : IsClosed s) (t_cl : IsClosed t) (st_dis : Disjoint s t) :

    This technique to witness HasSeparatingCover in regular Lindelöf topological spaces will be used to prove regular Lindelöf spaces are normal.

    theorem exists_compact_closed_between {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (h_KU : K U) :
    ∃ (L : Set X), IsCompact L IsClosed L K interior L L U

    In a (possibly non-Hausdorff) locally compact regular space, for every containment K ⊆ U of a compact set K in an open set U, there is a compact closed neighborhood L such that K ⊆ L ⊆ U: equivalently, there is a compact closed set L such that K ⊆ interior L and L ⊆ U.

    theorem exists_open_between_and_isCompact_closure {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X} (hK : IsCompact K) (hU : IsOpen U) (hKU : K U) :
    ∃ (V : Set X), IsOpen V K V closure V U IsCompact (closure V)

    In a locally compact regular space, given a compact set K inside an open set U, we can find an open set V between these sets with compact closure: K ⊆ V and the closure of V is inside U.

    class T25Space (X : Type u) [TopologicalSpace X] :

    A T₂.₅ space, also known as a Urysohn space, is a topological space where for every pair x ≠ y, there are two open sets, with the intersection of closures empty, one containing x and the other y .

    • t2_5 ⦃x y : X : x yDisjoint ((nhds x).lift' closure) ((nhds y).lift' closure)

      Given two distinct points in a T₂.₅ space, their filters of closed neighborhoods are disjoint.

    Instances
      @[simp]
      theorem disjoint_lift'_closure_nhds {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} :
      Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) x y
      @[instance 100]
      instance T25Space.t2Space {X : Type u_1} [TopologicalSpace X] [T25Space X] :
      theorem exists_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} (h : x y) :
      snhds x, tnhds y, Disjoint (closure s) (closure t)
      theorem exists_open_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {x y : X} (h : x y) :
      ∃ (u : Set X), x u IsOpen u ∃ (v : Set X), y v IsOpen v Disjoint (closure u) (closure v)
      theorem T25Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space Y] {f : XY} (hinj : Function.Injective f) (hcont : Continuous f) :
      @[deprecated Topology.IsEmbedding.t25Space (since := "2024-10-26")]
      theorem Embedding.t25Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T25Space Y] {f : XY} (hf : Topology.IsEmbedding f) :

      Alias of Topology.IsEmbedding.t25Space.

      instance Subtype.instT25Space {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : XProp} :
      T25Space { x : X // p x }
      class T3Space (X : Type u) [TopologicalSpace X] extends T0Space X, RegularSpace X :

      A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and a T₂.₅ space.

      Instances
        @[instance 90]
        instance instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] :
        @[instance 100]
        instance T3Space.t25Space {X : Type u_1} [TopologicalSpace X] [T3Space X] :
        theorem Topology.IsEmbedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : XY} (hf : Topology.IsEmbedding f) :
        @[deprecated Topology.IsEmbedding.t3Space (since := "2024-10-26")]
        theorem Embedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : XY} (hf : Topology.IsEmbedding f) :

        Alias of Topology.IsEmbedding.t3Space.

        instance Subtype.t3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] {p : XProp} :
        instance instT3SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] [T3Space Y] :
        T3Space (X × Y)
        instance instT3SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)] :
        T3Space ((i : ι) → X i)
        theorem disjoint_nested_nhds {X : Type u_1} [TopologicalSpace X] [T3Space X] {x y : X} (h : x y) :
        U₁nhds x, V₁nhds x, U₂nhds y, V₂nhds y, IsClosed V₁ IsClosed V₂ IsOpen U₁ IsOpen U₂ V₁ U₁ V₂ U₂ Disjoint U₁ U₂

        Given two points x ≠ y, we can find neighbourhoods x ∈ V₁ ⊆ U₁ and y ∈ V₂ ⊆ U₂, with the Vₖ closed and the Uₖ open, such that the Uₖ are disjoint.

        A topological space is said to be a normal space if any two disjoint closed sets have disjoint open neighborhoods.

        Instances
          theorem normal_separation {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) :
          theorem disjoint_nhdsSet_nhdsSet {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
          theorem normal_exists_closure_subset {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s t) :
          ∃ (u : Set X), IsOpen u s u closure u t

          If the codomain of a closed embedding is a normal space, then so is the domain.

          @[deprecated Topology.IsClosedEmbedding.normalSpace (since := "2024-10-20")]

          Alias of Topology.IsClosedEmbedding.normalSpace.


          If the codomain of a closed embedding is a normal space, then so is the domain.

          @[instance 100]

          A regular topological space with a Lindelöf topology is a normal space. A consequence of e.g. Corollaries 20.8 and 20.10 of [Willard's General Topology][zbMATH02107988] (without the assumption of Hausdorff).

          class T4Space (X : Type u) [TopologicalSpace X] extends T1Space X, NormalSpace X :

          A T₄ space is a normal T₁ space.

          Instances
            @[instance 100]
            instance T4Space.t3Space {X : Type u_1} [TopologicalSpace X] [T4Space X] :

            If the codomain of a closed embedding is a T₄ space, then so is the domain.

            @[deprecated Topology.IsClosedEmbedding.t4Space (since := "2024-10-20")]
            theorem ClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space Y] {f : XY} (hf : Topology.IsClosedEmbedding f) :

            Alias of Topology.IsClosedEmbedding.t4Space.


            If the codomain of a closed embedding is a T₄ space, then so is the domain.

            A topological space X is a completely normal space provided that for any two sets s, t such that if both closure s is disjoint with t, and s is disjoint with closure t, then there exist disjoint neighbourhoods of s and t.

            Instances
              @[instance 100]

              A completely normal space is a normal space.

              @[deprecated Topology.IsEmbedding.completelyNormalSpace (since := "2024-10-26")]

              Alias of Topology.IsEmbedding.completelyNormalSpace.

              A subspace of a completely normal space is a completely normal space.

              A T₅ space is a completely normal T₁ space.

              Instances
                theorem Topology.IsEmbedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : Topology.IsEmbedding e) :
                @[deprecated Topology.IsEmbedding.t5Space (since := "2024-10-26")]
                theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : Topology.IsEmbedding e) :

                Alias of Topology.IsEmbedding.t5Space.

                @[instance 100]
                instance T5Space.toT4Space {X : Type u_1} [TopologicalSpace X] [T5Space X] :

                A T₅ space is a T₄ space.

                instance instT5SpaceSubtype {X : Type u_1} [TopologicalSpace X] [T5Space X] {p : XProp} :
                T5Space { x : X // p x }

                A subspace of a T₅ space is a T₅ space.

                theorem connectedComponent_eq_iInter_isClopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (x : X) :
                connectedComponent x = ⋂ (s : { s : Set X // IsClopen s x s }), s

                In a compact T₂ space, the connected component of a point equals the intersection of all its clopen neighbourhoods.

                ConnectedComponents X is Hausdorff when X is Hausdorff and compact