Documentation

Mathlib.Topology.Separation

Separation properties of topological spaces. #

This file defines the predicate SeparatedNhds, and common separation axioms (under the Kolmogorov classification).

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.

TODOs #

Main results #

T₀ spaces #

T₁ spaces #

T₂ spaces #

If the space is also compact:

Regular spaces #

If the space is also Lindelöf:

T₃ spaces #

References #

def SeparatedNhds {X : Type u_1} [TopologicalSpace X] :
Set XSet XProp

SeparatedNhds is a predicate on pairs of subSets of a topological space. It holds if the two subSets are contained in disjoint open sets.

Equations
Instances For
    theorem SeparatedNhds.disjoint_nhdsSet {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} :

    Alias of the forward direction of separatedNhds_iff_disjoint.

    def HasSeparatingCover {X : Type u_1} [TopologicalSpace X] :
    Set XSet XProp

    HasSeparatingCovers can be useful witnesses for SeparatedNhds.

    Equations
    Instances For

      Used to prove that a regular topological space with Lindelöf topology is a normal space, and (todo) a perfectly normal space is a completely normal space.

      theorem SeparatedNhds.symm {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} :
      theorem SeparatedNhds.comm {X : Type u_1} [TopologicalSpace X] (s : Set X) (t : Set X) :
      theorem SeparatedNhds.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set Y} {t : Set Y} (h : SeparatedNhds s t) (hf : Continuous f) :
      theorem SeparatedNhds.disjoint {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : SeparatedNhds s t) :
      @[simp]
      theorem SeparatedNhds.mono {X : Type u_1} [TopologicalSpace X] {s₁ : Set X} {s₂ : Set X} {t₁ : Set X} {t₂ : Set X} (h : SeparatedNhds s₂ t₂) (hs : s₁ s₂) (ht : t₁ t₂) :
      SeparatedNhds s₁ t₁
      theorem SeparatedNhds.union_left {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} {u : Set X} :
      theorem SeparatedNhds.union_right {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} {u : Set X} (ht : SeparatedNhds s t) (hu : SeparatedNhds s u) :
      class T0Space (X : Type u) [TopologicalSpace X] :

      A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair x ≠ y, there is an open set containing one but not the other. We formulate the definition in terms of the Inseparable relation.

      • t0 : ∀ ⦃x y : X⦄, Inseparable x yx = y

        Two inseparable points in a T₀ space are equal.

      Instances
        theorem T0Space.t0 {X : Type u} [TopologicalSpace X] [self : T0Space X] ⦃x : X ⦃y : X :
        Inseparable x yx = y

        Two inseparable points in a T₀ space are equal.

        theorem t0Space_iff_inseparable (X : Type u) [TopologicalSpace X] :
        T0Space X ∀ (x y : X), Inseparable x yx = y
        theorem Inseparable.eq {X : Type u_1} [TopologicalSpace X] [T0Space X] {x : X} {y : X} (h : Inseparable x y) :
        x = y
        theorem Inducing.injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : XY} (hf : Inducing f) :

        A topology Inducing map from a T₀ space is injective.

        theorem Inducing.embedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : XY} (hf : Inducing f) :

        A topology Inducing map from a T₀ space is a topological embedding.

        theorem embedding_iff_inducing {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] {f : XY} :
        theorem inseparable_iff_eq {X : Type u_1} [TopologicalSpace X] [T0Space X] {x : X} {y : X} :
        Inseparable x y x = y
        @[simp]
        theorem nhds_eq_nhds_iff {X : Type u_1} [TopologicalSpace X] [T0Space X] {a : X} {b : X} :
        nhds a = nhds b a = b
        @[simp]
        theorem inseparable_eq_eq {X : Type u_1} [TopologicalSpace X] [T0Space X] :
        Inseparable = Eq
        theorem TopologicalSpace.IsTopologicalBasis.eq_iff {X : Type u_1} [TopologicalSpace X] [T0Space X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : X} {y : X} :
        x = y sb, x s y s
        theorem t0Space_iff_exists_isOpen_xor'_mem (X : Type u) [TopologicalSpace X] :
        T0Space X Pairwise fun (x y : X) => ∃ (U : Set X), IsOpen U Xor' (x U) (y U)
        theorem exists_isOpen_xor'_mem {X : Type u_1} [TopologicalSpace X] [T0Space X] {x : X} {y : X} (h : x y) :
        ∃ (U : Set X), IsOpen U Xor' (x U) (y U)

        Specialization forms a partial order on a t0 topological space.

        Equations
        Instances For
          theorem minimal_nonempty_closed_subsingleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s) (hmin : ts, t.NonemptyIsClosed tt = s) :
          s.Subsingleton
          theorem minimal_nonempty_closed_eq_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s) (hne : s.Nonempty) (hmin : ts, t.NonemptyIsClosed tt = s) :
          ∃ (x : X), s = {x}
          theorem IsClosed.exists_closed_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] [CompactSpace X] {S : Set X} (hS : IsClosed S) (hne : S.Nonempty) :
          xS, IsClosed {x}

          Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.

          theorem minimal_nonempty_open_subsingleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s) (hmin : ts, t.NonemptyIsOpen tt = s) :
          s.Subsingleton
          theorem minimal_nonempty_open_eq_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s) (hne : s.Nonempty) (hmin : ts, t.NonemptyIsOpen tt = s) :
          ∃ (x : X), s = {x}
          theorem exists_isOpen_singleton_of_isOpen_finite {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hfin : s.Finite) (hne : s.Nonempty) (ho : IsOpen s) :
          xs, IsOpen {x}

          Given an open finite set S in a T₀ space, there is some x ∈ S such that {x} is open.

          theorem exists_open_singleton_of_finite {X : Type u_1} [TopologicalSpace X] [T0Space X] [Finite X] [Nonempty X] :
          ∃ (x : X), IsOpen {x}
          theorem t0Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] :
          theorem Embedding.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] {f : XY} (hf : Embedding f) :
          instance Subtype.t0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] {p : XProp} :
          Equations
          • =
          theorem t0Space_iff_or_not_mem_closure (X : Type u) [TopologicalSpace X] :
          T0Space X Pairwise fun (a b : X) => aclosure {b} bclosure {a}
          instance Prod.instT0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space X] [T0Space Y] :
          T0Space (X × Y)
          Equations
          • =
          instance Pi.instT0Space {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T0Space (X i)] :
          T0Space ((i : ι) → X i)
          Equations
          • =
          Equations
          • =
          theorem T0Space.of_cover {X : Type u_1} [TopologicalSpace X] (h : ∀ (x y : X), Inseparable x y∃ (s : Set X), x s y s T0Space s) :
          theorem T0Space.of_open_cover {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∃ (s : Set X), x s IsOpen s T0Space s) :
          theorem r0Space_iff (X : Type u) [TopologicalSpace X] :
          R0Space X Symmetric Specializes
          class R0Space (X : Type u) [TopologicalSpace X] :

          A topological space is called an R₀ space, if Specializes relation is symmetric.

          In other words, given two points x y : X, if every neighborhood of y contains x, then every neighborhood of x contains y.

          • specializes_symmetric : Symmetric Specializes

            In an R₀ space, the Specializes relation is symmetric.

          Instances
            theorem R0Space.specializes_symmetric {X : Type u} [TopologicalSpace X] [self : R0Space X] :
            Symmetric Specializes

            In an R₀ space, the Specializes relation is symmetric.

            theorem Specializes.symm {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} {y : X} (h : x y) :
            y x

            In an R₀ space, the Specializes relation is symmetric, dot notation version.

            theorem specializes_comm {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} {y : X} :
            x y y x

            In an R₀ space, the Specializes relation is symmetric, Iff version.

            theorem specializes_iff_inseparable {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} {y : X} :

            In an R₀ space, Specializes is equivalent to Inseparable.

            theorem Specializes.inseparable {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} {y : X} :
            x yInseparable x y

            In an R₀ space, Specializes implies Inseparable.

            theorem Inducing.r0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R0Space X] [TopologicalSpace Y] {f : YX} (hf : Inducing f) :
            instance instR0SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R0Space X] {p : XProp} :
            R0Space { x : X // p x }
            Equations
            • =
            instance instR0SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R0Space X] [TopologicalSpace Y] [R0Space Y] :
            R0Space (X × Y)
            Equations
            • =
            instance instR0SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R0Space (X i)] :
            R0Space ((i : ι) → X i)
            Equations
            • =

            In an R₀ space, the closure of a singleton is a compact set.

            In an R₀ space, relatively compact sets form a bornology. Its cobounded filter is Filter.coclosedCompact. See also Bornology.inCompact the bornology of sets contained in a compact set.

            Equations
            Instances For
              theorem Set.Finite.isCompact_closure {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} (hs : s.Finite) :

              In an R₀ space, the closure of a finite set is a compact set.

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

              A T₁ space, also known as a Fréchet space, is a topological space where every singleton set is closed. Equivalently, for every pair x ≠ y, there is an open set containing x and not y.

              • t1 : ∀ (x : X), IsClosed {x}

                A singleton in a T₁ space is a closed set.

              Instances
                theorem T1Space.t1 {X : Type u} [TopologicalSpace X] [self : T1Space X] (x : X) :

                A singleton in a T₁ space is a closed set.

                theorem isClosed_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} :
                theorem isOpen_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} :
                theorem isOpen_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} :
                IsOpen {y : X | y x}
                theorem Continuous.isOpen_support {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [Zero X] [TopologicalSpace Y] {f : YX} (hf : Continuous f) :
                theorem Continuous.isOpen_mulSupport {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [One X] [TopologicalSpace Y] {f : YX} (hf : Continuous f) :
                theorem Ne.nhdsWithin_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x y) :
                theorem Ne.nhdsWithin_diff_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x y) (s : Set X) :
                nhdsWithin x (s \ {y}) = nhdsWithin x s
                theorem nhdsWithin_compl_singleton_le {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) (y : X) :
                theorem isOpen_setOf_eventually_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {p : XProp} :
                IsOpen {x : X | ∀ᶠ (y : X) in nhdsWithin x {x}, p y}
                theorem Set.Finite.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : s.Finite) :
                theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : X} {y : X} (h : x y) :
                ab, x a ya
                theorem Finset.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) :
                theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
                [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}, Continuous CofiniteTopology.of, ∀ ⦃x y : X⦄, x y{y} nhds x, ∀ ⦃x y : X⦄, x ysnhds x, ys, ∀ ⦃x y : X⦄, x y∃ (U : Set X), IsOpen U x U yU, ∀ ⦃x y : X⦄, x yDisjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x yDisjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x yx = y].TFAE
                theorem CofiniteTopology.continuous_of {X : Type u_1} [TopologicalSpace X] [T1Space X] :
                Continuous CofiniteTopology.of
                theorem t1Space_iff_exists_open {X : Type u_1} [TopologicalSpace X] :
                T1Space X Pairwise fun (x y : X) => ∃ (U : Set X), IsOpen U x U yU
                theorem t1Space_iff_disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] :
                T1Space X ∀ ⦃x y : X⦄, x yDisjoint (pure x) (nhds y)
                theorem t1Space_iff_disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] :
                T1Space X ∀ ⦃x y : X⦄, x yDisjoint (nhds x) (pure y)
                theorem t1Space_iff_specializes_imp_eq {X : Type u_1} [TopologicalSpace X] :
                T1Space X ∀ ⦃x y : X⦄, x yx = y
                theorem disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x y) :
                theorem disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x y) :
                theorem Specializes.eq {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x y) :
                x = y
                theorem specializes_iff_eq {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} :
                x y x = y
                @[simp]
                theorem specializes_eq_eq {X : Type u_1} [TopologicalSpace X] [T1Space X] :
                (fun (x x_1 : X) => x x_1) = Eq
                @[simp]
                theorem pure_le_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {a : X} {b : X} :
                pure a nhds b a = b
                @[simp]
                theorem nhds_le_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {a : X} {b : X} :
                nhds a nhds b a = b
                @[instance 100]
                Equations
                • =
                Equations
                • =
                theorem continuousWithinAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : XY} {s : Set X} {x : X} {x' : X} {y : Y} (hne : x' x) :
                theorem continuousAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : XY} {x : X} {x' : X} {y : Y} (hne : x' x) :
                theorem continuousOn_update_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : XY} {s : Set X} {x : X} {y : Y} :
                ContinuousOn (Function.update f x y) s ContinuousOn f (s \ {x}) (x sFilter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y))
                theorem t1Space_of_injective_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] :
                theorem Embedding.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : XY} (hf : Embedding f) :
                instance Subtype.t1Space {X : Type u} [TopologicalSpace X] [T1Space X] {p : XProp} :
                Equations
                • =
                instance instT1SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [T1Space Y] :
                T1Space (X × Y)
                Equations
                • =
                instance instT1SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] :
                T1Space ((i : ι) → X i)
                Equations
                • =
                Equations
                • =
                @[instance 100]
                Equations
                • =
                @[instance 100]
                instance T1Space.t0Space {X : Type u_1} [TopologicalSpace X] [T1Space X] :
                Equations
                • =
                @[simp]
                theorem compl_singleton_mem_nhds_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} :
                {x} nhds y y x
                theorem compl_singleton_mem_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : y x) :
                {x} nhds y
                @[simp]
                theorem closure_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} :
                closure {x} = {x}
                theorem Set.Subsingleton.closure {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : s.Subsingleton) :
                (closure s).Subsingleton
                @[simp]
                theorem subsingleton_closure {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} :
                (closure s).Subsingleton s.Subsingleton
                theorem nhdsWithin_insert_of_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} {s : Set X} (hxy : x y) :
                theorem insert_mem_nhdsWithin_of_subset_insert {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} {s : Set X} {t : Set X} (hu : t insert y s) :

                If t is a subset of s, except for one point, then insert x s is a neighborhood of x within t.

                @[simp]
                theorem ker_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) :
                (nhds x).ker = {x}
                theorem biInter_basis_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {ι : Sort u_3} {p : ιProp} {s : ιSet X} {x : X} (h : (nhds x).HasBasis p s) :
                ⋂ (i : ι), ⋂ (_ : p i), s i = {x}
                @[simp]
                theorem compl_singleton_mem_nhdsSet_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {s : Set X} :
                {x} nhdsSet s xs
                @[simp]
                theorem nhdsSet_le_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {t : Set X} :
                @[simp]
                theorem nhdsSet_inj_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {t : Set X} :
                @[simp]
                theorem nhds_le_nhdsSet_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {x : X} :
                theorem Dense.diff_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (hs : Dense s) (x : X) [(nhdsWithin x {x}).NeBot] :
                Dense (s \ {x})

                Removing a non-isolated point from a dense set, one still obtains a dense set.

                theorem Dense.diff_finset {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}).NeBot] {s : Set X} (hs : Dense s) (t : Finset X) :
                Dense (s \ t)

                Removing a finset from a dense set in a space without isolated points, one still obtains a dense set.

                theorem Dense.diff_finite {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) :
                Dense (s \ t)

                Removing a finite set from a dense set in a space without isolated points, one still obtains a dense set.

                theorem eq_of_tendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : XY} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) :
                f x = y

                If a function to a T1Space tends to some limit y at some point x, then necessarily y = f x.

                theorem Filter.Tendsto.eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] [T1Space Y] {g : XY} {l : Filter X} {b₁ : Y} {b₂ : Y} (hg : Filter.Tendsto g l (nhds b₁)) (hb : b₁ b₂) :
                ∀ᶠ (z : X) in l, g z b₂
                theorem ContinuousAt.eventually_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {g : XY} {x : X} {y : Y} (hg1 : ContinuousAt g x) (hg2 : g x y) :
                ∀ᶠ (z : X) in nhds x, g z y
                theorem eventually_ne_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {a : X} {b : X} (h : a b) :
                ∀ᶠ (x : X) in nhds a, x b
                theorem eventually_ne_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {a : X} {b : X} {s : Set X} (h : a b) :
                ∀ᶠ (x : X) in nhdsWithin a s, x b
                theorem continuousAt_of_tendsto_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : XY} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) :

                To prove a function to a T1Space is continuous at some point x, it suffices to prove that f admits some limit at x.

                @[simp]
                theorem tendsto_const_nhds_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] {l : Filter Y} [l.NeBot] {c : X} {d : X} :
                Filter.Tendsto (fun (x : Y) => c) l (nhds d) c = d
                theorem isOpen_singleton_of_finite_mem_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] (x : X) {s : Set X} (hs : s nhds x) (hsf : s.Finite) :
                IsOpen {x}

                A point with a finite neighborhood has to be isolated.

                theorem infinite_of_mem_nhds {X : Type u_3} [TopologicalSpace X] [T1Space X] (x : X) [hx : (nhdsWithin x {x}).NeBot] {s : Set X} (hs : s nhds x) :
                s.Infinite

                If the punctured neighborhoods of a point form a nontrivial filter, then any neighborhood is infinite.

                theorem IsPreconnected.infinite_of_nontrivial {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} (h : IsPreconnected s) (hs : s.Nontrivial) :
                s.Infinite
                @[instance 100]

                A non-trivial connected T1 space has no isolated points.

                Equations
                • =
                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) :
                theorem singleton_mem_nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology s] {x : X} (hx : x s) :
                {x} nhdsWithin x s
                theorem nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology s] {x : X} (hx : x s) :

                The neighbourhoods filter of x within s, under the discrete topology, is equal to the pure x filter (which is the principal filter at the singleton {x}.)

                theorem Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : ιProp} {t : ιSet X} {s : Set X} [DiscreteTopology s] {x : X} (hb : (nhds x).HasBasis p t) (hx : x s) :
                ∃ (i : ι), p i t i s = {x}
                theorem nhds_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology s] {x : X} (hx : x s) :
                Unhds x, U s = {x}

                A point x in a discrete subset s of a topological space admits a neighbourhood that only meets s at x.

                theorem isOpen_inter_eq_singleton_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology s] {x : X} (hx : x s) :
                ∃ (U : Set X), IsOpen U U s = {x}

                Let x be a point in a discrete subset s of a topological space, then there exists an open set that only meets s at x.

                theorem disjoint_nhdsWithin_of_mem_discrete {X : Type u_1} [TopologicalSpace X] {s : Set X} [DiscreteTopology s] {x : X} (hx : x s) :
                UnhdsWithin x {x}, Disjoint U s

                For point x in a discrete subset s of a topological space, there is a set U such that

                1. U is a punctured neighborhood of x (ie. U ∪ {x} is a neighbourhood of x),
                2. U is disjoint from s.
                theorem closedEmbedding_update {ι : Type u_3} {β : ιType u_4} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)] :

                R₁ (preregular) spaces #

                class R1Space (X : Type u_3) [TopologicalSpace X] :

                A topological space is called a preregular (a.k.a. R₁) space, if any two topologically distinguishable points have disjoint neighbourhoods.

                Instances
                  theorem R1Space.specializes_or_disjoint_nhds {X : Type u_3} [TopologicalSpace X] [self : R1Space X] (x : X) (y : X) :
                  x y Disjoint (nhds x) (nhds y)
                  @[instance 100]
                  instance instR0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] :
                  Equations
                  • =
                  theorem specializes_iff_not_disjoint {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {y : X} :
                  x y ¬Disjoint (nhds x) (nhds y)
                  theorem isClosed_setOf_specializes {X : Type u_1} [TopologicalSpace X] [R1Space X] :
                  IsClosed {p : X × X | p.1 p.2}
                  theorem IsCompact.mem_closure_iff_exists_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {y : X} {K : Set X} (hK : IsCompact K) :
                  y closure K xK, Inseparable x y

                  In an R₁ space, a point belongs to the closure of a compact set K if and only if it is topologically inseparable from some point of K.

                  theorem IsCompact.closure_eq_biUnion_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) :
                  closure K = xK, {y : X | Inseparable x y}
                  theorem IsCompact.closure_eq_biUnion_closure_singleton {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) :
                  closure K = xK, closure {x}

                  In an R₁ space, the closure of a compact set is the union of the closures of its points.

                  theorem IsCompact.closure_subset_of_isOpen {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) {U : Set X} (hU : IsOpen U) (hKU : K U) :

                  In an R₁ space, if a compact set K is contained in an open set U, then its closure is also contained in U.

                  theorem IsCompact.closure {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} (hK : IsCompact K) :

                  The closure of a compact set in an R₁ space is a compact set.

                  theorem IsCompact.closure_of_subset {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} {K : Set X} (hK : IsCompact K) (h : s K) :
                  @[deprecated IsCompact.closure_of_subset]
                  theorem isCompact_closure_of_subset_compact {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} {K : Set X} (hK : IsCompact K) (h : s K) :

                  Alias of IsCompact.closure_of_subset.

                  @[simp]
                  theorem exists_isCompact_superset_iff {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} :
                  (∃ (K : Set X), IsCompact K s K) IsCompact (closure s)
                  @[deprecated exists_isCompact_superset_iff]
                  theorem exists_compact_superset_iff {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} :
                  (∃ (K : Set X), IsCompact K s K) IsCompact (closure s)

                  Alias of exists_isCompact_superset_iff.

                  theorem SeparatedNhds.of_isCompact_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} {L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) :

                  If K and L are disjoint compact sets in an R₁ topological space and L is also closed, then K and L have disjoint neighborhoods.

                  @[deprecated SeparatedNhds.of_isCompact_isCompact_isClosed]
                  theorem separatedNhds_of_isCompact_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} {L : Set X} (hK : IsCompact K) (hL : IsCompact L) (h'L : IsClosed L) (hd : Disjoint K L) :

                  Alias of SeparatedNhds.of_isCompact_isCompact_isClosed.


                  If K and L are disjoint compact sets in an R₁ topological space and L is also closed, then K and L have disjoint neighborhoods.

                  theorem IsCompact.binary_compact_cover {X : Type u_1} [TopologicalSpace X] [R1Space X] {K : Set X} {U : Set X} {V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K U V) :
                  ∃ (K₁ : Set X) (K₂ : Set X), IsCompact K₁ IsCompact K₂ K₁ U K₂ V K = K₁ K₂

                  If a compact set is covered by two open sets, then we can cover it by two compact subsets.

                  theorem IsCompact.finite_compact_cover {X : Type u_1} [TopologicalSpace X] [R1Space X] {s : Set X} (hs : IsCompact s) {ι : Type u_3} (t : Finset ι) (U : ιSet X) (hU : it, IsOpen (U i)) (hsC : s it, U i) :
                  ∃ (K : ιSet X), (∀ (i : ι), IsCompact (K i)) (∀ (i : ι), K i U i) s = it, K i

                  For every finite open cover Uᵢ of a compact set, there exists a compact cover Kᵢ ⊆ Uᵢ.

                  theorem R1Space.of_continuous_specializes_imp {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : YX} (hc : Continuous f) (hspec : ∀ (x y : Y), f x f yx y) :
                  theorem Inducing.r1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : YX} (hf : Inducing f) :
                  theorem R1Space.induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] (f : YX) :
                  instance instR1SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R1Space X] (p : XProp) :
                  Equations
                  • =
                  theorem R1Space.sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (hT : tT, R1Space X) :
                  theorem R1Space.iInf {ι : Type u_3} {X : Type u_4} {t : ιTopologicalSpace X} (ht : ∀ (i : ι), R1Space X) :
                  theorem R1Space.inf {X : Type u_3} {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} (h₁ : R1Space X) (h₂ : R1Space X) :
                  instance instR1SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] [R1Space Y] :
                  R1Space (X × Y)
                  Equations
                  • =
                  instance instR1SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), R1Space (X i)] :
                  R1Space ((i : ι) → X i)
                  Equations
                  • =
                  theorem exists_mem_nhds_isCompact_mapsTo_of_isCompact_mem_nhds {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [R1Space Y] {f : XY} {x : X} {K : Set X} {s : Set Y} (hf : Continuous f) (hs : s nhds (f x)) (hKc : IsCompact K) (hKx : K nhds x) :
                  Knhds x, IsCompact K Set.MapsTo f K s
                  theorem IsCompact.isCompact_isClosed_basis_nhds {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {L : Set X} (hLc : IsCompact L) (hxL : L nhds x) :
                  (nhds x).HasBasis (fun (K : Set X) => K nhds x IsCompact K IsClosed K) fun (x : Set X) => x

                  If a point in an R₁ space has a compact neighborhood, then it has a basis of compact closed neighborhoods.

                  @[simp]

                  In an R₁ space, the filters coclosedCompact and cocompact are equal.

                  @[simp]

                  In an R₁ space, the bornologies relativelyCompact and inCompact are equal.

                  Lemmas about a weakly locally compact R₁ space #

                  In fact, a space with these properties is locally compact and regular. Some lemmas are formulated using the latter assumptions below.

                  theorem isCompact_isClosed_basis_nhds {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) :
                  (nhds x).HasBasis (fun (K : Set X) => K nhds x IsCompact K IsClosed K) fun (x : Set X) => x

                  In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point x form a basis of neighborhoods of x.

                  In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood.

                  @[instance 80]

                  A weakly locally compact R₁ space is locally compact.

                  Equations
                  • =

                  In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure.

                  @[deprecated exists_isOpen_superset_and_isCompact_closure]

                  Alias of exists_isOpen_superset_and_isCompact_closure.


                  In a weakly locally compact R₁ space, every compact set has an open neighborhood with compact closure.

                  In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.

                  @[deprecated exists_isOpen_mem_isCompact_closure]

                  Alias of exists_isOpen_mem_isCompact_closure.


                  In a weakly locally compact R₁ space, every point has an open neighborhood with compact closure.

                  theorem t2Space_iff (X : Type u) [TopologicalSpace X] :
                  T2Space X Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u IsOpen v x u y v Disjoint u v
                  class T2Space (X : Type u) [TopologicalSpace X] :

                  A T₂ space, also known as a Hausdorff space, is one in which for every x ≠ y there exists disjoint open sets around x and y. This is the most widely used of the separation axioms.

                  Instances
                    theorem T2Space.t2 {X : Type u} [TopologicalSpace X] [self : T2Space X] :
                    Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u IsOpen v x u y v Disjoint u v

                    Every two points in a Hausdorff space admit disjoint open neighbourhoods.

                    theorem t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {y : X} (h : x y) :
                    ∃ (u : Set X) (v : Set X), IsOpen u IsOpen v x u y v Disjoint u v

                    Two different points can be separated by open sets.

                    theorem t2Space_iff_disjoint_nhds {X : Type u_1} [TopologicalSpace X] :
                    T2Space X Pairwise fun (x y : X) => Disjoint (nhds x) (nhds y)
                    @[simp]
                    theorem disjoint_nhds_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {y : X} :
                    Disjoint (nhds x) (nhds y) x y
                    theorem pairwise_disjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] :
                    Pairwise (Disjoint on nhds)
                    theorem Set.pairwiseDisjoint_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Set X) :
                    s.PairwiseDisjoint nhds
                    theorem Set.Finite.t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : s.Finite) :
                    ∃ (U : XSet X), (∀ (x : X), x U x IsOpen (U x)) s.PairwiseDisjoint U

                    Points of a finite set can be separated by open sets from each other.

                    @[instance 100]
                    instance T2Space.t1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
                    Equations
                    • =
                    @[instance 100]
                    instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
                    Equations
                    • =
                    @[instance 80]
                    Equations
                    • =
                    theorem t2_iff_nhds {X : Type u_1} [TopologicalSpace X] :
                    T2Space X ∀ {x y : X}, (nhds x nhds y).NeBotx = y

                    A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.

                    theorem eq_of_nhds_neBot {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {y : X} (h : (nhds x nhds y).NeBot) :
                    x = y
                    theorem t2Space_iff_nhds {X : Type u_1} [TopologicalSpace X] :
                    T2Space X Pairwise fun (x y : X) => Unhds x, Vnhds y, Disjoint U V
                    theorem t2_separation_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {y : X} (h : x y) :
                    ∃ (u : Set X) (v : Set X), u nhds x v nhds y Disjoint u v
                    theorem t2_separation_compact_nhds {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {x : X} {y : X} (h : x y) :
                    ∃ (u : Set X) (v : Set X), u nhds x v nhds y IsCompact u IsCompact v Disjoint u v
                    theorem t2_iff_ultrafilter {X : Type u_1} [TopologicalSpace X] :
                    T2Space X ∀ {x y : X} (f : Ultrafilter X), f nhds xf nhds yx = y
                    theorem tendsto_nhds_unique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : YX} {l : Filter Y} {a : X} {b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) :
                    a = b
                    theorem tendsto_nhds_unique' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : YX} {l : Filter Y} {a : X} {b : X} :
                    l.NeBotFilter.Tendsto f l (nhds a)Filter.Tendsto f l (nhds b)a = b
                    theorem tendsto_nhds_unique_of_eventuallyEq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : YX} {g : YX} {l : Filter Y} {a : X} {b : X} [l.NeBot] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : f =ᶠ[l] g) :
                    a = b
                    theorem tendsto_nhds_unique_of_frequently_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : YX} {g : YX} {l : Filter Y} {a : X} {b : X} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : ∃ᶠ (x : Y) in l, f x = g x) :
                    a = b
                    theorem IsCompact.nhdsSet_inter_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) :

                    If s and t are compact sets in a T₂ space, then the set neighborhoods filter of s ∩ t is the infimum of set neighborhoods filters for s and t.

                    For general sets, only the inequality holds, see nhdsSet_inter_le.

                    theorem Set.InjOn.exists_mem_nhdsSet {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : xs, ContinuousAt f x) (loc : xs, unhds x, Set.InjOn f u) :
                    tnhdsSet s, Set.InjOn f t

                    If a function f is

                    • injective on a compact set s;
                    • continuous at every point of this set;
                    • injective on a neighborhood of each point of this set,

                    then it is injective on a neighborhood of this set.

                    theorem Set.InjOn.exists_isOpen_superset {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : xs, ContinuousAt f x) (loc : xs, unhds x, Set.InjOn f u) :
                    ∃ (t : Set X), IsOpen t s t Set.InjOn f t

                    If a function f is

                    • injective on a compact set s;
                    • continuous at every point of this set;
                    • injective on a neighborhood of each point of this set,

                    then it is injective on an open neighborhood of this set.

                    Properties of lim and limUnder #

                    In this section we use explicit Nonempty X instances for lim and limUnder. This way the lemmas are useful without a Nonempty X instance.

                    theorem lim_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Filter X} {x : X} [f.NeBot] (h : f nhds x) :
                    lim f = x
                    theorem lim_eq_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Filter X} [f.NeBot] (h : ∃ (x : X), f nhds x) {x : X} :
                    lim f = x f nhds x
                    theorem Ultrafilter.lim_eq_iff_le_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X} :
                    F.lim = x F nhds x
                    theorem isOpen_iff_ultrafilter' {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] (U : Set X) :
                    IsOpen U ∀ (F : Ultrafilter X), F.lim UU F
                    theorem Filter.Tendsto.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {x : X} {f : Filter Y} [f.NeBot] {g : YX} (h : Filter.Tendsto g f (nhds x)) :
                    limUnder f g = x
                    theorem Filter.limUnder_eq_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Filter Y} [f.NeBot] {g : YX} (h : ∃ (x : X), Filter.Tendsto g f (nhds x)) {x : X} :
                    theorem Continuous.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] {f : YX} (h : Continuous f) (y : Y) :
                    limUnder (nhds y) f = f y
                    @[simp]
                    theorem lim_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) :
                    lim (nhds x) = x
                    @[simp]
                    theorem limUnder_nhds_id {X : Type u_1} [TopologicalSpace X] [T2Space X] (x : X) :
                    limUnder (nhds x) id = x
                    @[simp]
                    theorem lim_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Set X} (h : x closure s) :
                    lim (nhdsWithin x s) = x
                    @[simp]
                    theorem limUnder_nhdsWithin_id {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Set X} (h : x closure s) :
                    limUnder (nhdsWithin x s) id = x

                    T2Space constructions #

                    We use two lemmas to prove that various standard constructions generate Hausdorff spaces from Hausdorff spaces:

                    @[instance 100]
                    Equations
                    • =
                    theorem separated_by_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) {x : X} {y : X} (h : f x f y) :
                    ∃ (u : Set X) (v : Set X), IsOpen u IsOpen v x u y v Disjoint u v
                    theorem separated_by_openEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : XY} (hf : OpenEmbedding f) {x : X} {y : X} (h : x y) :
                    ∃ (u : Set Y) (v : Set Y), IsOpen u IsOpen v f x u f y v Disjoint u v
                    instance instT2SpaceSubtype {X : Type u_1} [TopologicalSpace X] {p : XProp} [T2Space X] :
                    Equations
                    • =
                    instance Prod.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] :
                    T2Space (X × Y)
                    Equations
                    • =
                    theorem T2Space.of_injective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hinj : Function.Injective f) (hc : Continuous f) :

                    If the codomain of an injective continuous function is a Hausdorff space, then so is its domain.

                    theorem Embedding.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Embedding f) :

                    If the codomain of a topological embedding is a Hausdorff space, then so is its domain. See also T2Space.of_continuous_injective.

                    Equations
                    • =
                    instance instT2SpaceSum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] :
                    T2Space (X Y)
                    Equations
                    • =
                    instance Pi.t2Space {X : Type u_1} {Y : XType v} [(a : X) → TopologicalSpace (Y a)] [∀ (a : X), T2Space (Y a)] :
                    T2Space ((a : X) → Y a)
                    Equations
                    • =
                    instance Sigma.t2Space {ι : Type u_4} {X : ιType u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)] :
                    T2Space ((i : ι) × X i)
                    Equations
                    • =
                    def t2Setoid (X : Type u_1) [TopologicalSpace X] :

                    The smallest equivalence relation on a topological space giving a T2 quotient.

                    Equations
                    Instances For
                      def t2Quotient (X : Type u_1) [TopologicalSpace X] :
                      Type u_1

                      The largest T2 quotient of a topological space. This construction is left-adjoint to the inclusion of T2 spaces into all topological spaces.

                      Equations
                      Instances For
                        def t2Quotient.mk {X : Type u_1} [TopologicalSpace X] :
                        Xt2Quotient X

                        The map from a topological space to its largest T2 quotient.

                        Equations
                        Instances For
                          theorem t2Quotient.mk_eq {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
                          t2Quotient.mk x = t2Quotient.mk y ∀ (s : Setoid X), T2Space (Quotient s)s.Rel x y
                          theorem t2Quotient.continuous_mk (X : Type u_1) [TopologicalSpace X] :
                          Continuous t2Quotient.mk
                          theorem t2Quotient.inductionOn {X : Type u_1} [TopologicalSpace X] {motive : t2Quotient XProp} (q : t2Quotient X) (h : ∀ (x : X), motive (t2Quotient.mk x)) :
                          motive q
                          theorem t2Quotient.inductionOn₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {motive : t2Quotient Xt2Quotient YProp} (q : t2Quotient X) (q' : t2Quotient Y) (h : ∀ (x : X) (y : Y), motive (t2Quotient.mk x) (t2Quotient.mk y)) :
                          motive q q'

                          The largest T2 quotient of a topological space is indeed T2.

                          Equations
                          • =
                          theorem t2Quotient.compatible {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) (a : X) (b : X) :
                          a bf a = f b
                          def t2Quotient.lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) :
                          t2Quotient XY

                          The universal property of the largest T2 quotient of a topological space X: any continuous map from X to a T2 space Y uniquely factors through t2Quotient X. This declaration builds the factored map. Its continuity is t2Quotient.continuous_lift, the fact that it indeed factors the original map is t2Quotient.lift_mk and uniquenes is t2Quotient.unique_lift.

                          Equations
                          Instances For
                            theorem t2Quotient.continuous_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) :
                            @[simp]
                            theorem t2Quotient.lift_mk {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) (x : X) :
                            theorem t2Quotient.unique_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : XY} (hf : Continuous f) {g : t2Quotient XY} (hfg : g t2Quotient.mk = f) :
                            theorem isClosed_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : YX} {g : YX} (hf : Continuous f) (hg : Continuous g) :
                            IsClosed {y : Y | f y = g y}
                            theorem isOpen_ne_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : YX} {g : YX} (hf : Continuous f) (hg : Continuous g) :
                            IsOpen {y : Y | f y g y}
                            theorem Set.EqOn.closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {s : Set Y} {f : YX} {g : YX} (h : Set.EqOn f g s) (hf : Continuous f) (hg : Continuous g) :

                            If two continuous maps are equal on s, then they are equal on the closure of s. See also Set.EqOn.of_subset_closure for a more general version.

                            theorem Continuous.ext_on {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {s : Set Y} (hs : Dense s) {f : YX} {g : YX} (hf : Continuous f) (hg : Continuous g) (h : Set.EqOn f g s) :
                            f = g

                            If two continuous functions are equal on a dense set, then they are equal.

                            theorem eqOn_closure₂' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f : XYZ} {g : XYZ} (h : xs, yt, f x y = g x y) (hf₁ : ∀ (x : X), Continuous (f x)) (hf₂ : ∀ (y : Y), Continuous fun (x : X) => f x y) (hg₁ : ∀ (x : X), Continuous (g x)) (hg₂ : ∀ (y : Y), Continuous fun (x : X) => g x y) (x : X) :
                            x closure syclosure t, f x y = g x y
                            theorem eqOn_closure₂ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] [T2Space Z] {s : Set X} {t : Set Y} {f : XYZ} {g : XYZ} (h : xs, yt, f x y = g x y) (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) (x : X) :
                            x closure syclosure t, f x y = g x y
                            theorem Set.EqOn.of_subset_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s : Set X} {t : Set X} {f : XY} {g : XY} (h : Set.EqOn f g s) (hf : ContinuousOn f t) (hg : ContinuousOn g t) (hst : s t) (hts : t closure s) :
                            Set.EqOn f g t

                            If f x = g x for all x ∈ s and f, g are continuous on t, s ⊆ t ⊆ closure s, then f x = g x for all x ∈ t. See also Set.EqOn.closure.

                            theorem Function.LeftInverse.isClosed_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : XY} {g : YX} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
                            @[deprecated Function.LeftInverse.isClosed_range]
                            theorem Function.LeftInverse.closed_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : XY} {g : YX} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :

                            Alias of Function.LeftInverse.isClosed_range.

                            theorem Function.LeftInverse.closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : XY} {g : YX} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
                            theorem SeparatedNhds.of_isCompact_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) :
                            @[deprecated SeparatedNhds.of_isCompact_isCompact]
                            theorem separatedNhds_of_isCompact_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) :

                            Alias of SeparatedNhds.of_isCompact_isCompact.

                            theorem SeparatedNhds.of_finset_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Finset X) (t : Finset X) (h : Disjoint s t) :
                            SeparatedNhds s t
                            @[deprecated SeparatedNhds.of_finset_finset]
                            theorem separatedNhds_of_finset_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Finset X) (t : Finset X) (h : Disjoint s t) :
                            SeparatedNhds s t

                            Alias of SeparatedNhds.of_finset_finset.

                            theorem SeparatedNhds.of_singleton_finset {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Finset X} (h : xs) :
                            SeparatedNhds {x} s
                            @[deprecated SeparatedNhds.of_singleton_finset]
                            theorem point_disjoint_finset_opens_of_t2 {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {s : Finset X} (h : xs) :
                            SeparatedNhds {x} s

                            Alias of SeparatedNhds.of_singleton_finset.

                            theorem IsCompact.isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : IsCompact s) :

                            In a T2Space, every compact set is closed.

                            theorem IsCompact.preimage_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : XY} {s : Set Y} (hs : IsCompact s) (hf : Continuous f) :
                            theorem Pi.isCompact_iff {ι : Type u_4} {π : ιType u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} :
                            theorem Pi.isCompact_closure_iff {ι : Type u_4} {π : ιType u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} :
                            theorem exists_subset_nhds_of_isCompact {X : Type u_1} [TopologicalSpace X] [T2Space X] {ι : Type u_4} [Nonempty ι] {V : ιSet X} (hV : Directed (fun (x x_1 : Set X) => x x_1) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) {U : Set X} (hU : x⋂ (i : ι), V i, U nhds x) :
                            ∃ (i : ι), V i U

                            If V : ι → Set X is a decreasing family of compact sets then any neighborhood of ⋂ i, V i contains some V i. This is a version of exists_subset_nhds_of_isCompact' where we don't need to assume each V i closed because it follows from compactness since X is assumed to be Hausdorff.

                            theorem IsCompact.inter {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
                            theorem image_closure_of_isCompact {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : XY} (hf : ContinuousOn f (closure s)) :
                            f '' closure s = closure (f '' s)
                            theorem Continuous.isClosedMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : XY} (h : Continuous f) :

                            A continuous map from a compact space to a Hausdorff space is a closed map.

                            theorem Continuous.closedEmbedding {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : XY} (h : Continuous f) (hf : Function.Injective f) :

                            A continuous injective map from a compact space to a Hausdorff space is a closed embedding.

                            theorem QuotientMap.of_surjective_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompactSpace X] [T2Space Y] {f : XY} (hsurj : Function.Surjective f) (hcont : Continuous f) :

                            A continuous surjective map from a compact space to a Hausdorff space is a quotient map.

                            theorem IsPreirreducible.subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (h : IsPreirreducible S) :
                            S.Subsingleton
                            theorem isIrreducible_iff_singleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} :
                            IsIrreducible S ∃ (x : X), S = {x}

                            There does not exist a nontrivial preirreducible T₂ space.

                            theorem regularSpace_iff (X : Type u) [TopologicalSpace X] :
                            RegularSpace X ∀ {s : Set X} {a : X}, IsClosed sasDisjoint (nhdsSet s) (nhds a)

                            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.regular {X : Type u} [TopologicalSpace X] [self : RegularSpace X] {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.

                              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) :
                              @[deprecated RegularSpace.of_lift'_closure]
                              theorem RegularSpace.ofLift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), (nhds x).lift' closure = nhds x) :

                              Alias of RegularSpace.of_lift'_closure.

                              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)) :
                              @[deprecated RegularSpace.of_hasBasis]
                              theorem RegularSpace.ofBasis {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)) :

                              Alias of RegularSpace.of_hasBasis.

                              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) :
                              @[deprecated RegularSpace.of_exists_mem_nhds_isClosed_subset]
                              theorem RegularSpace.ofExistsMemNhdsIsClosedSubset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), snhds x, tnhds x, IsClosed t t s) :

                              Alias of RegularSpace.of_exists_mem_nhds_isClosed_subset.

                              @[instance 100]

                              A weakly locally compact R₁ space is regular.

                              Equations
                              • =
                              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₁.

                              Equations
                              • =
                              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 : Set X} {U : Set X} (hK : IsCompact K) (hU : U nhdsSet K) :
                              ∃ (V : Set X), IsOpen V K V closure V U
                              theorem IsCompact.lift'_closure_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {K : Set X} (hK : IsCompact K) :
                              (nhdsSet K).lift' closure = nhdsSet K
                              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
                              theorem Inducing.regularSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] {f : YX} (hf : Inducing f) :
                              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₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} (h₁ : RegularSpace X) (h₂ : RegularSpace X) :
                              Equations
                              • =
                              Equations
                              • =
                              instance instRegularSpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] :
                              RegularSpace ((i : ι) → X i)
                              Equations
                              • =
                              theorem SeparatedNhds.of_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {s : Set X} {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.

                              @[deprecated SeparatedNhds.of_isCompact_isClosed]
                              theorem separatedNhds_of_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :

                              Alias of SeparatedNhds.of_isCompact_isClosed.


                              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 : Set X} {t : Set X} [r : RegularSpace X] [LindelofSpace 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 : Set X} {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 : Set X} {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.

                              @[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]
                              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
                                theorem T25Space.t2_5 {X : Type u} [TopologicalSpace X] [self : T25Space X] ⦃x : 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.

                                @[simp]
                                theorem disjoint_lift'_closure_nhds {X : Type u_1} [TopologicalSpace X] [T25Space X] {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] :
                                Equations
                                • =
                                theorem exists_nhds_disjoint_closure {X : Type u_1} [TopologicalSpace X] [T25Space X] {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 : 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) :
                                instance instT25SpaceSubtype {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : XProp} :
                                T25Space { x : X // p x }
                                Equations
                                • =
                                class T3Space (X : Type u) [TopologicalSpace X] extends T0Space , RegularSpace :

                                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] :
                                    Equations
                                    • =
                                    @[instance 100]
                                    instance T3Space.t25Space {X : Type u_1} [TopologicalSpace X] [T3Space X] :
                                    Equations
                                    • =
                                    theorem Embedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : XY} (hf : Embedding f) :
                                    instance Subtype.t3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] {p : XProp} :
                                    Equations
                                    • =
                                    Equations
                                    • =
                                    instance instT3SpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] [T3Space Y] :
                                    T3Space (X × Y)
                                    Equations
                                    • =
                                    instance instT3SpaceForall {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)] :
                                    T3Space ((i : ι) → X i)
                                    Equations
                                    • =
                                    theorem disjoint_nested_nhds {X : Type u_1} [TopologicalSpace X] [T3Space X] {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.

                                    The SeparationQuotient of a regular space is a T₃ space.

                                    Equations
                                    • =

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

                                    Instances
                                      theorem NormalSpace.normal {X : Type u} [TopologicalSpace X] [self : NormalSpace X] (s : Set X) (t : Set X) :
                                      IsClosed sIsClosed tDisjoint s tSeparatedNhds s t

                                      Two disjoint sets in a normal space admit disjoint neighbourhoods.

                                      theorem normal_separation {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s : Set X} {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 : Set X} {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 : Set X} {t : Set X} (hs : IsClosed s) (ht : IsOpen t) (hst : s t) :
                                      ∃ (u : Set X), IsOpen u s u closure u t
                                      theorem ClosedEmbedding.normalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y] {f : XY} (hf : ClosedEmbedding f) :

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

                                      @[instance 100]
                                      Equations
                                      • =
                                      @[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).

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

                                      A T₄ space is a normal T₁ space.

                                        Instances
                                          @[instance 100]
                                          Equations
                                          • =
                                          @[instance 100]
                                          instance T4Space.t3Space {X : Type u_1} [TopologicalSpace X] [T4Space X] :
                                          Equations
                                          • =
                                          @[deprecated inferInstance]
                                          theorem ClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space Y] {f : XY} (hf : ClosedEmbedding f) :

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

                                          Equations
                                          • =

                                          The SeparationQuotient of a normal space is a normal space.

                                          Equations
                                          • =

                                          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
                                            theorem CompletelyNormalSpace.completely_normal {X : Type u} [TopologicalSpace X] [self : CompletelyNormalSpace X] ⦃s : Set X ⦃t : Set X :

                                            If closure s is disjoint with t, and s is disjoint with closure t, then s and t admit disjoint neighbourhoods.

                                            @[instance 100]

                                            A completely normal space is a normal space.

                                            Equations
                                            • =

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

                                            Equations
                                            • =

                                            A T₅ space is a normal T₁ space.

                                              Instances
                                                theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : Embedding e) :
                                                @[instance 100]
                                                instance T5Space.toT4Space {X : Type u_1} [TopologicalSpace X] [T5Space X] :

                                                A T₅ space is a T₄ space.

                                                Equations
                                                • =
                                                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.

                                                Equations
                                                • =
                                                Equations
                                                • =

                                                The SeparationQuotient of a completely normal R₀ space is a T₅ space.

                                                Equations
                                                • =
                                                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.

                                                A T1 space with a clopen basis is totally separated.

                                                A compact Hausdorff space is totally disconnected if and only if it is totally separated, this is also true for locally compact spaces.

                                                @[instance 100]

                                                A totally disconnected compact Hausdorff space is totally separated.

                                                Equations
                                                • =
                                                theorem nhds_basis_clopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] (x : X) :
                                                (nhds x).HasBasis (fun (s : Set X) => x s IsClopen s) id
                                                theorem compact_exists_isClopen_in_isOpen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] {x : X} {U : Set X} (is_open : IsOpen U) (memU : x U) :
                                                ∃ (V : Set X), IsClopen V x V V U

                                                Every member of an open set in a compact Hausdorff totally disconnected space is contained in a clopen set contained in the open set.

                                                A locally compact Hausdorff totally disconnected space has a basis with clopen elements.

                                                A locally compact Hausdorff space is totally disconnected if and only if it is totally separated.

                                                ConnectedComponents X is Hausdorff when X is Hausdorff and compact

                                                Equations
                                                • =