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 #

Main results #

T₀ spaces #

T₁ spaces #

T₂ spaces #

If the space is also compact:

T₃ spaces #

References #

https://en.wikipedia.org/wiki/Separation_axiom

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.

    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_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, Set.Nonempty tIsClosed tt = s) :
        theorem minimal_nonempty_closed_eq_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s) (hne : Set.Nonempty s) (hmin : ts, Set.Nonempty tIsClosed 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 : Set.Nonempty S) :
        ∃ x ∈ S, 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, Set.Nonempty tIsOpen tt = s) :
        theorem minimal_nonempty_open_eq_singleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsOpen s) (hne : Set.Nonempty s) (hmin : ts, Set.Nonempty tIsOpen 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 : Set.Finite s) (hne : Set.Nonempty s) (ho : IsOpen s) :
        ∃ x ∈ s, 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 containx y.

        • specializes_symmetric : Symmetric Specializes

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

        Instances
          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 instR0SpaceSubtypeInstTopologicalSpaceSubtype {X : Type u_1} [TopologicalSpace X] [R0Space X] {p : XProp} :
          R0Space { x : X // p x }
          Equations
          • =
          Equations
          • =
          instance instR0SpaceForAllTopologicalSpace {ι : 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

            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 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 : Set.Finite s) :
              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) :
              ∃ a ∈ b, 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] :
              List.TFAE [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 y∃ s ∈ nhds 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]
              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 instR0Space {X : Type u_1} [TopologicalSpace X] [T1Space X] :
              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
              • =
              Equations
              • =
              instance instT1SpaceForAllTopologicalSpace {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] :
              T1Space ((i : ι) → X i)
              Equations
              • =
              Equations
              • =
              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 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) :
              Filter.ker (nhds x) = {x}
              theorem biInter_basis_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {ι : Sort u_3} {p : ιProp} {s : ιSet X} {x : X} (h : Filter.HasBasis (nhds x) 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) [Filter.NeBot (nhdsWithin x {x})] :
              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), Filter.NeBot (nhdsWithin x {x})] {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), Filter.NeBot (nhdsWithin x {x})] {s : Set X} (hs : Dense s) {t : Set X} (ht : Set.Finite t) :
              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} [Filter.NeBot l] {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 : Set.Finite s) :
              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 : Filter.NeBot (nhdsWithin x {x})] {s : Set X} (hs : s nhds x) :

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

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

              Equations
              • =
              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 : Filter.HasBasis (nhds x) 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) :
              ∃ U ∈ nhds 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) :
              ∃ U ∈ nhdsWithin 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.
              @[deprecated embedding_inclusion]
              theorem TopologicalSpace.subset_trans {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (ts : t s) :
              instTopologicalSpaceSubtype = TopologicalSpace.induced (Set.inclusion ts) instTopologicalSpaceSubtype

              Let X be a topological space and let s, t ⊆ X be two subsets. If there is an inclusion t ⊆ s, then the topological space structure on t induced by X is the same as the one obtained by the induced topological space structure on s. Use embedding_inclusion instead.

              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
                instance instR0Space_1 {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 ∃ x ∈ K, 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 = ⋃ x ∈ K, {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 = ⋃ x ∈ K, 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 ⋃ i ∈ t, U i) :
                ∃ (K : ιSet X), (∀ (i : ι), IsCompact (K i)) (∀ (i : ι), K i U i) s = ⋃ i ∈ t, 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) :
                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) :
                Equations
                • =
                instance instR1SpaceForAllTopologicalSpace {ι : 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) :
                ∃ K ∈ nhds 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) :
                Filter.HasBasis (nhds x) (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) :
                Filter.HasBasis (nhds x) (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.

                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 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.Finite.t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : Set.Finite s) :
                  ∃ (U : XSet X), (∀ (x : X), x U x IsOpen (U x)) Set.PairwiseDisjoint s U

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

                  instance T2Space.t1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
                  Equations
                  • =
                  instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] :
                  Equations
                  • =
                  instance instT2Space {X : Type u_1} [TopologicalSpace X] [R1Space X] [T0Space X] :
                  Equations
                  • =
                  theorem t2_iff_nhds {X : Type u_1} [TopologicalSpace X] :
                  T2Space X ∀ {x y : X}, Filter.NeBot (nhds x nhds y)x = 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 : Filter.NeBot (nhds x nhds y)) :
                  x = y
                  theorem t2Space_iff_nhds {X : Type u_1} [TopologicalSpace X] :
                  T2Space X Pairwise fun (x y : X) => ∃ U ∈ nhds x, ∃ V ∈ nhds 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} [Filter.NeBot l] (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} :
                  Filter.NeBot lFilter.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} [Filter.NeBot l] (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 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, ∃ u ∈ nhds x, Set.InjOn f u) :
                  ∃ t ∈ nhdsSet 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, ∃ u ∈ nhds 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.

                  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 .

                  Instances
                    @[simp]
                    theorem disjoint_lift'_closure_nhds {X : Type u_1} [TopologicalSpace X] [T25Space X] {x : X} {y : X} :
                    Disjoint (Filter.lift' (nhds x) closure) (Filter.lift' (nhds y) closure) x y
                    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) :
                    ∃ s ∈ nhds x, ∃ t ∈ nhds 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 instT25SpaceSubtypeInstTopologicalSpaceSubtype {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : XProp} :
                    T25Space { x : X // p x }
                    Equations
                    • =

                    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} [Filter.NeBot f] (h : f nhds x) :
                    lim f = x
                    theorem lim_eq_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] {f : Filter X} [Filter.NeBot f] (h : ∃ (x : X), f nhds x) {x : X} :
                    lim f = 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), Ultrafilter.lim F UU F
                    theorem Filter.Tendsto.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {x : X} {f : Filter Y} [Filter.NeBot f] {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} [Filter.NeBot f] {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:

                    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
                    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
                    • =
                    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
                    • =
                    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 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_TFAE (X : Type u) [TopologicalSpace X] :
                      List.TFAE [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, ∃ t ∈ nhds x, IsClosed t t s, ∀ (x : X), Filter.lift' (nhds x) closure nhds x, ∀ (x : X), Filter.lift' (nhds x) closure = nhds x]
                      theorem RegularSpace.of_lift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), Filter.lift' (nhds x) closure = nhds x) :
                      @[deprecated RegularSpace.of_lift'_closure]
                      theorem RegularSpace.ofLift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), Filter.lift' (nhds x) 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), Filter.HasBasis (nhds a) (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), Filter.HasBasis (nhds a) (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, ∃ t ∈ nhds 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, ∃ t ∈ nhds x, IsClosed t t s) :

                      Alias of RegularSpace.of_exists_mem_nhds_isClosed_subset.

                      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 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) :
                      ∃ t ∈ nhds x, IsClosed t t s
                      theorem closed_nhds_basis {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
                      Filter.HasBasis (nhds x) (fun (s : Set X) => s nhds x IsClosed s) id
                      theorem lift'_nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
                      Filter.lift' (nhds x) 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 : Filter.HasBasis (nhds x) p s) :
                      Filter.HasBasis (nhds x) p fun (i : ι) => closure (s i)
                      theorem hasBasis_nhds_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
                      Filter.HasBasis (nhds x) (fun (s : Set X) => s nhds x) closure
                      theorem hasBasis_opens_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] (x : X) :
                      Filter.HasBasis (nhds x) (fun (s : Set X) => x s IsOpen s) 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) :
                      instance instRegularSpaceForAllTopologicalSpace {ι : 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 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 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 instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] :
                          Equations
                          • =
                          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
                          • =
                          Equations
                          • =
                          instance instT3SpaceForAllTopologicalSpace {ι : 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.

                          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 : 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.

                            A regular topological space with second countable topology is a normal space.

                            TODO: The same is true for a regular Lindelöf space.

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

                            A T₄ space is a normal T₁ space.

                              Instances
                                instance instT4Space {X : Type u_1} [TopologicalSpace X] [T1Space X] [NormalSpace X] :
                                Equations
                                • =
                                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
                                • =
                                class T5Space (X : Type u) [TopologicalSpace X] extends T1Space :

                                A topological space X is a completely normal Hausdorff space if each subspace s : Set X is a normal Hausdorff space. Equivalently, X is a T₁ space and for any two sets s, t such that closure s is disjoint with t and s is disjoint with closure t, there exist disjoint neighbourhoods of s and t.

                                Instances
                                  theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : XY} (he : Embedding e) :
                                  instance instT5SpaceSubtypeInstTopologicalSpaceSubtype {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
                                  • =
                                  instance T5Space.toT4Space {X : Type u_1} [TopologicalSpace X] [T5Space X] :

                                  A T₅ space is a T₄ space.

                                  Equations
                                  • =

                                  The SeparationQuotient of a completely normal R₀ space is a T₅ space. We don't have typeclasses for completely normal spaces (without T₁ assumption) and R₀ spaces, so we use T5Space for assumption and for conclusion.

                                  One can prove this using a homeomorphism between X and SeparationQuotient X. We give an alternative proof of the completely_normal axiom that works without assuming that X 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.

                                  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) :
                                  Filter.HasBasis (nhds x) (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
                                  • =