Separation properties of topological spaces.

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

Main definitions

• SeparatedNhds: Two Sets are separated by neighbourhoods if they are contained in disjoint open sets.
• HasSeparatingCover: A set has a countable cover that can be used with hasSeparatingCovers_iff_separatedNhds to witness when two Sets have SeparatedNhds.
• T0Space: A T₀/Kolmogorov space is a space where, for every two points x ≠ y, there is an open set that contains one, but not the other.
• R0Space: An R₀ space (sometimes called a symmetric space) is a topological space such that the Specializes relation is symmetric.
• T1Space: A T₁/Fréchet space is a space where every singleton set is closed. This is equivalent to, for every pair x ≠ y, there existing an open set containing x but not y (t1Space_iff_exists_open shows that these conditions are equivalent.) T₁ implies T₀ and R₀.
• R1Space: An R₁/preregular space is a space where any two topologically distinguishable points have disjoint neighbourhoods. R₁ implies R₀.
• T2Space: A T₂/Hausdorff space is a space where, for every two points x ≠ y, there is two disjoint open sets, one containing x, and the other y. T₂ implies T₁ and R₁.
• T25Space: A T₂.₅/Urysohn space is a space where, for every two points x ≠ y, there is two open sets, one containing x, and the other y, whose closures are disjoint. T₂.₅ implies T₂.
• RegularSpace: A regular space is one where, given any closed C and x ∉ C, there are disjoint open sets containing x and C respectively. Such a space is not necessarily Hausdorff.
• T3Space: A T₃ space is a regular T₀ space. T₃ implies T₂.₅.
• NormalSpace: A normal space, is one where given two disjoint closed sets, we can find two open sets that separate them. Such a space is not necessarily Hausdorff, even if it is T₀.
• T4Space: A T₄ space is a normal T₁ space. T₄ implies T₃.
• CompletelyNormalSpace: A completely normal space is one in which 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. Embedding.completelyNormalSpace allows us to conclude that this is equivalent to all subspaces being normal. Such a space is not necessarily Hausdorff or regular, even if it is T₀.
• T5Space: A T₅ space is a completely normal T₁ space. T₅ implies T₄.

Note that mathlib adopts the modern convention that m ≤ n if and only if T_m → T_n, but occasionally the literature swaps definitions for e.g. T₃ and regular.

TODOs

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

Main results

T₀ spaces

• IsClosed.exists_closed_singleton: Given a closed set S in a compact T₀ space, there is some x ∈ S such that {x} is closed.
• exists_isOpen_singleton_of_isOpen_finite: Given an open finite set S in a T₀ space, there is some x ∈ S such that {x} is open.

T₁ spaces

• isClosedMap_const: The constant map is a closed map.
• discrete_of_t1_of_finite: A finite T₁ space must have the discrete topology.

T₂ spaces

• t2_iff_nhds: A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter.
• t2_iff_isClosed_diagonal: A space is T₂ iff the diagonal of X (that is, the set of all points of the form (a, a) : X × X) is closed under the product topology.
• separatedNhds_of_finset_finset: Any two disjoint finsets are SeparatedNhds.
• Most topological constructions preserve Hausdorffness; these results are part of the typeclass inference system (e.g. Embedding.t2Space)
• Set.EqOn.closure: If two functions are equal on some set s, they are equal on its closure.
• IsCompact.isClosed: All compact sets are closed.
• WeaklyLocallyCompactSpace.locallyCompactSpace: If a topological space is both weakly locally compact (i.e., each point has a compact neighbourhood) and is T₂, then it is locally compact.
• totallySeparatedSpace_of_t1_of_basis_clopen: If X has a clopen basis, then it is a TotallySeparatedSpace.
• loc_compact_t2_tot_disc_iff_tot_sep: A locally compact T₂ space is totally disconnected iff it is totally separated.
• t2Quotient: the largest T2 quotient of a given topological space.

If the space is also compact:

• normalOfCompactT2: A compact T₂ space is a NormalSpace.
• connectedComponent_eq_iInter_isClopen: The connected component of a point is the intersection of all its clopen neighbourhoods.
• compact_t2_tot_disc_iff_tot_sep: Being a TotallyDisconnectedSpace is equivalent to being a TotallySeparatedSpace.
• ConnectedComponents.t2: ConnectedComponents X is T₂ for X T₂ and compact.

Regular spaces

If the space is also Lindelöf:

• NormalSpace.of_regularSpace_lindelofSpace: every regular Lindelöf space is normal.

T₃ spaces

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

References

• https://en.wikipedia.org/wiki/Separation_axiom
• https://en.wikipedia.org/wiki/Normal_space
• [Willard's General Topology][zbMATH02107988]

def SeparatedNhds {X : Type u_1} [TopologicalSpace X] : Set X → Set X → Prop

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

• SeparatedNhds s t = ∃ (U : Set X) (V : Set X), IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ Disjoint U V

theorem separatedNhds_iff_disjoint {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} : SeparatedNhds s t ↔ Disjoint (nhdsSet s) (nhdsSet t)

theorem SeparatedNhds.disjoint_nhdsSet {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} : SeparatedNhds s t → Disjoint (nhdsSet s) (nhdsSet t)

Alias of the forward direction of separatedNhds_iff_disjoint.

def HasSeparatingCover {X : Type u_1} [TopologicalSpace X] : Set X → Set X → Prop

HasSeparatingCovers can be useful witnesses for SeparatedNhds.

Equations

• HasSeparatingCover s t = ∃ (u : ℕ → Set X), s ⊆ ⋃ (n : ℕ), u n ∧ ∀ (n : ℕ), IsOpen (u n) ∧ Disjoint (closure (u n)) t

theorem hasSeparatingCovers_iff_separatedNhds {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} : HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

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} : SeparatedNhds s t → SeparatedNhds t s

theorem SeparatedNhds.comm {X : Type u_1} [TopologicalSpace X] (s : Set X) (t : Set X) : SeparatedNhds s t ↔ SeparatedNhds t s

theorem SeparatedNhds.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} {t : Set Y} (h : SeparatedNhds s t) (hf : Continuous f) : SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)

theorem SeparatedNhds.disjoint {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : SeparatedNhds s t) : Disjoint s t

theorem SeparatedNhds.disjoint_closure_left {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : SeparatedNhds s t) : Disjoint (closure s) t

theorem SeparatedNhds.disjoint_closure_right {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} (h : SeparatedNhds s t) : Disjoint s (closure t)

@[simp]

theorem SeparatedNhds.empty_right {X : Type u_1} [TopologicalSpace X] (s : Set X) : SeparatedNhds s ∅

@[simp]

theorem SeparatedNhds.empty_left {X : Type u_1} [TopologicalSpace X] (s : Set X) : SeparatedNhds ∅ s

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} : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

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) : SeparatedNhds s (t ∪ u)

class T0Space (X : Type u) [TopologicalSpace X] : Prop

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 y → x = y

  Two inseparable points in a T₀ space are equal.

theorem T0Space.t0 {X : Type u} [TopologicalSpace X] [self : T0Space X] ⦃x : X⦄ ⦃y : X⦄ : Inseparable x y → x = 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 y → x = y

theorem t0Space_iff_not_inseparable (X : Type u) [TopologicalSpace X] : T0Space X ↔ Pairwise fun (x y : X) => ¬Inseparable x 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 : X → Y} (hf : Inducing f) : Function.Injective 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 : X → Y} (hf : Inducing f) : Embedding 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 : X → Y} : Embedding f ↔ Inducing f

theorem t0Space_iff_nhds_injective (X : Type u) [TopologicalSpace X] : T0Space X ↔ Function.Injective nhds

theorem nhds_injective {X : Type u_1} [TopologicalSpace X] [T0Space X] : Function.Injective nhds

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.inseparable_iff {X : Type u_1} [TopologicalSpace X] {b : Set (Set X)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : X} {y : X} : Inseparable x y ↔ ∀ s ∈ b, x ∈ s ↔ y ∈ s

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 ↔ ∀ s ∈ b, 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)

def specializationOrder (X : Type u_3) [TopologicalSpace X] [T0Space X] : PartialOrder X

Specialization forms a partial order on a t0 topological space.

Equations

• specializationOrder X = let __src := specializationPreorder X; let __src_1 := PartialOrder.lift (⇑OrderDual.toDual ∘ nhds) ⋯; PartialOrder.mk ⋯

instance SeparationQuotient.instT0Space {X : Type u_1} [TopologicalSpace X] : T0Space (SeparationQuotient X)

Equations

• ⋯ = ⋯

theorem minimal_nonempty_closed_subsingleton {X : Type u_1} [TopologicalSpace X] [T0Space X] {s : Set X} (hs : IsClosed s) (hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = 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 : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = 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) : ∃ 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 : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = 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 : ∀ t ⊆ s, t.Nonempty → IsOpen t → t = 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) : ∃ 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 : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T0Space Y] : T0Space X

theorem Embedding.t0Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T0Space Y] {f : X → Y} (hf : Embedding f) : T0Space X

instance Subtype.t0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] {p : X → Prop} : T0Space (Subtype p)

Equations

• ⋯ = ⋯

theorem t0Space_iff_or_not_mem_closure (X : Type u) [TopologicalSpace X] : T0Space X ↔ Pairwise fun (a b : X) => a ∉ closure {b} ∨ b ∉ closure {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

• ⋯ = ⋯

instance ULift.instT0Space {X : Type u_1} [TopologicalSpace X] [T0Space X] : T0Space (ULift.{u_3, u_1} X)

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) : T0Space X

theorem T0Space.of_open_cover {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∃ (s : Set X), x ∈ s ∧ IsOpen s ∧ T0Space ↑s) : T0Space X

theorem r0Space_iff (X : Type u) [TopologicalSpace X] : R0Space X ↔ Symmetric Specializes

class R0Space (X : Type u) [TopologicalSpace X] : Prop

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.

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} : x ⤳ y ↔ Inseparable x y

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 ⤳ y → Inseparable 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 : Y → X} (hf : Inducing f) : R0Space Y

instance instR0SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R0Space X] {p : X → Prop} : 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

• ⋯ = ⋯

theorem isCompact_closure_singleton {X : Type u_1} [TopologicalSpace X] [R0Space X] {x : X} : IsCompact (closure {x})

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

theorem Filter.coclosedCompact_le_cofinite {X : Type u_1} [TopologicalSpace X] [R0Space X] : Filter.coclosedCompact X ≤ Filter.cofinite

def Bornology.relativelyCompact (X : Type u_1) [TopologicalSpace X] [R0Space X] : Bornology X

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

• Bornology.relativelyCompact X = { cobounded' := Filter.coclosedCompact X, le_cofinite' := ⋯ }

theorem Bornology.relativelyCompact.isBounded_iff {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} : Bornology.IsBounded s ↔ IsCompact (closure s)

theorem Set.Finite.isCompact_closure {X : Type u_1} [TopologicalSpace X] [R0Space X] {s : Set X} (hs : s.Finite) : IsCompact (closure s)

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

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

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.

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

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

theorem isClosed_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsClosed {x}

theorem isOpen_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} : IsOpen {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 : Y → X} (hf : Continuous f) : IsOpen (Function.support f)

theorem Continuous.isOpen_mulSupport {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [One X] [TopologicalSpace Y] {f : Y → X} (hf : Continuous f) : IsOpen (Function.mulSupport f)

theorem Ne.nhdsWithin_compl_singleton {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x ≠ y) : nhdsWithin x {y}ᶜ = nhds x

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) : nhdsWithin x {x}ᶜ ≤ nhdsWithin x {y}ᶜ

theorem isOpen_setOf_eventually_nhdsWithin {X : Type u_1} [TopologicalSpace X] [T1Space X] {p : X → Prop} : 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) : IsClosed 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 ∧ y ∉ a

theorem Finset.isClosed {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) : IsClosed ↑s

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 ≠ y → ∃ s ∈ nhds x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE

theorem t1Space_iff_continuous_cofinite_of {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ Continuous ⇑CofiniteTopology.of

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 ∧ y ∉ U

theorem t1Space_iff_disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y)

theorem t1Space_iff_disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y)

theorem t1Space_iff_specializes_imp_eq {X : Type u_1} [TopologicalSpace X] : T1Space X ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y

theorem disjoint_pure_nhds {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x ≠ y) : Disjoint (pure x) (nhds y)

theorem disjoint_nhds_pure {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} (h : x ≠ y) : Disjoint (nhds x) (pure 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]

instance instR0SpaceOfT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : R0Space X

Equations

• ⋯ = ⋯

instance instT1SpaceCofiniteTopology {X : Type u_1} : T1Space (CofiniteTopology X)

Equations

• ⋯ = ⋯

theorem t1Space_antitone {X : Type u_1} : Antitone (@T1Space X)

theorem continuousWithinAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {x' : X} {y : Y} (hne : x' ≠ x) : ContinuousWithinAt (Function.update f x y) s x' ↔ ContinuousWithinAt f s x'

theorem continuousAt_update_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {x : X} {x' : X} {y : Y} (hne : x' ≠ x) : ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x'

theorem continuousOn_update_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T1Space X] [DecidableEq X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {y : Y} : ContinuousOn (Function.update f x y) s ↔ ContinuousOn f (s \ {x}) ∧ (x ∈ s → Filter.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 : X → Y} (hf : Function.Injective f) (hf' : Continuous f) [T1Space Y] : T1Space X

theorem Embedding.t1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {f : X → Y} (hf : Embedding f) : T1Space X

instance Subtype.t1Space {X : Type u} [TopologicalSpace X] [T1Space X] {p : X → Prop} : T1Space (Subtype p)

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

• ⋯ = ⋯

instance ULift.instT1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T1Space (ULift.{u_3, u_1} X)

Equations

• ⋯ = ⋯

@[instance 100]

instance TotallyDisconnectedSpace.t1Space {X : Type u_1} [TopologicalSpace X] [h : TotallyDisconnectedSpace X] : T1Space X

Equations

• ⋯ = ⋯

@[instance 100]

instance T1Space.t0Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T0Space 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 isClosedMap_const {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] {y : Y} : IsClosedMap (Function.const X y)

theorem nhdsWithin_insert_of_ne {X : Type u_1} [TopologicalSpace X] [T1Space X] {x : X} {y : X} {s : Set X} (hxy : x ≠ y) : nhdsWithin x (insert y s) = nhdsWithin x s

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) : insert x s ∈ nhdsWithin x t

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 ↔ x ∉ s

@[simp]

theorem nhdsSet_le_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {t : Set X} : nhdsSet s ≤ nhdsSet t ↔ s ⊆ t

@[simp]

theorem nhdsSet_inj_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {t : Set X} : nhdsSet s = nhdsSet t ↔ s = t

theorem injective_nhdsSet {X : Type u_1} [TopologicalSpace X] [T1Space X] : Function.Injective nhdsSet

theorem strictMono_nhdsSet {X : Type u_1} [TopologicalSpace X] [T1Space X] : StrictMono nhdsSet

@[simp]

theorem nhds_le_nhdsSet_iff {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} {x : X} : nhds x ≤ nhdsSet s ↔ x ∈ s

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 : X → Y} {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 : X → Y} {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 : X → Y} {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 : X → Y} {x : X} {y : Y} (h : Filter.Tendsto f (nhds x) (nhds y)) : ContinuousAt f x

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 discrete_of_t1_of_finite {X : Type u_1} [TopologicalSpace X] [T1Space X] [Finite X] : DiscreteTopology X

theorem PreconnectedSpace.trivial_of_discrete {X : Type u_1} [TopologicalSpace X] [PreconnectedSpace X] [DiscreteTopology X] : Subsingleton X

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

theorem ConnectedSpace.infinite {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] : Infinite X

@[instance 100]

instance ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space {X : Type u_1} [TopologicalSpace X] [ConnectedSpace X] [Nontrivial X] [T1Space X] (x : X) : (nhdsWithin x {x}ᶜ).NeBot

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] : IsGδ {x}ᶜ

@[deprecated IsGδ.compl_singleton]

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

Alias of IsGδ.compl_singleton.

theorem Set.Countable.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Countable) : IsGδ sᶜ

theorem Set.Finite.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Finite) : IsGδ sᶜ

theorem Set.Subsingleton.isGδ_compl {X : Type u_1} [TopologicalSpace X] {s : Set X} [T1Space X] (hs : s.Subsingleton) : IsGδ sᶜ

theorem Finset.isGδ_compl {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Finset X) : IsGδ (↑s)ᶜ

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

@[deprecated IsGδ.singleton]

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

Alias of IsGδ.singleton.

theorem Set.Finite.isGδ {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} [T1Space X] (hs : s.Finite) : IsGδ s

theorem SeparationQuotient.t1Space_iff {X : Type u_1} [TopologicalSpace X] : T1Space (SeparationQuotient X) ↔ R0Space X

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) : nhdsWithin x s = pure x

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

theorem closedEmbedding_update {ι : Type u_3} {β : ι → Type u_4} [DecidableEq ι] [(i : ι) → TopologicalSpace (β i)] (x : (i : ι) → β i) (i : ι) [∀ (i : ι), T1Space (β i)] : ClosedEmbedding (Function.update x i)

R₁ (preregular) spaces

theorem r1Space_iff_specializes_or_disjoint_nhds (X : Type u_3) [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)

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

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

• specializes_or_disjoint_nhds : ∀ (x y : X), x ⤳ y ∨ Disjoint (nhds x) (nhds y)

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] : R0Space X

Equations

• ⋯ = ⋯

theorem disjoint_nhds_nhds_iff_not_specializes {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {y : X} : Disjoint (nhds x) (nhds y) ↔ ¬x ⤳ y

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 disjoint_nhds_nhds_iff_not_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] {x : X} {y : X} : Disjoint (nhds x) (nhds y) ↔ ¬Inseparable x y

theorem r1Space_iff_inseparable_or_disjoint_nhds {X : Type u_3} [TopologicalSpace X] : R1Space X ↔ ∀ (x y : X), Inseparable 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 isClosed_setOf_inseparable {X : Type u_1} [TopologicalSpace X] [R1Space X] : IsClosed {p : X × X | Inseparable 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) : closure 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) : IsCompact (closure 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) : IsCompact (closure s)

@[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) : IsCompact (closure s)

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) : SeparatedNhds 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) : SeparatedNhds 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 : ∀ i ∈ t, 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 : Y → X} (hc : Continuous f) (hspec : ∀ (x y : Y), f x ⤳ f y → x ⤳ y) : R1Space Y

theorem Inducing.r1Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] [TopologicalSpace Y] {f : Y → X} (hf : Inducing f) : R1Space Y

theorem R1Space.induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [R1Space X] (f : Y → X) : R1Space Y

instance instR1SpaceSubtype {X : Type u_1} [TopologicalSpace X] [R1Space X] (p : X → Prop) : R1Space (Subtype p)

Equations

• ⋯ = ⋯

theorem R1Space.sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (hT : ∀ t ∈ T, R1Space X) : R1Space X

theorem R1Space.iInf {ι : Type u_3} {X : Type u_4} {t : ι → TopologicalSpace X} (ht : ∀ (i : ι), R1Space X) : R1Space X

theorem R1Space.inf {X : Type u_3} {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} (h₁ : R1Space X) (h₂ : R1Space X) : 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 : X → Y} {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

@[instance 900]

instance instLocallyCompactPairOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [TopologicalSpace Y] [R1Space Y] : LocallyCompactPair X Y

Equations

• ⋯ = ⋯

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]

theorem Filter.coclosedCompact_eq_cocompact {X : Type u_1} [TopologicalSpace X] [R1Space X] : Filter.coclosedCompact X = Filter.cocompact X

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

@[simp]

theorem Bornology.relativelyCompact_eq_inCompact {X : Type u_1} [TopologicalSpace X] [R1Space X] : Bornology.relativelyCompact X = Bornology.inCompact X

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.

theorem exists_mem_nhds_isCompact_isClosed {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K

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

@[instance 80]

instance WeaklyLocallyCompactSpace.locallyCompactSpace {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] : LocallyCompactSpace X

A weakly locally compact R₁ space is locally compact.

Equations

• ⋯ = ⋯

theorem exists_isOpen_superset_and_isCompact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

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

@[deprecated exists_isOpen_superset_and_isCompact_closure]

theorem exists_open_superset_and_isCompact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] {K : Set X} (hK : IsCompact K) : ∃ (V : Set X), IsOpen V ∧ K ⊆ V ∧ IsCompact (closure V)

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.

theorem exists_isOpen_mem_isCompact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

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

@[deprecated exists_isOpen_mem_isCompact_closure]

theorem exists_open_with_compact_closure {X : Type u_1} [TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X) : ∃ (U : Set X), IsOpen U ∧ x ∈ U ∧ IsCompact (closure U)

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] : Prop

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.

• t2 : 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 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 : X → Set 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] : T1Space X

Equations

• ⋯ = ⋯

@[instance 100]

instance T2Space.r1Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : R1Space X

Equations

• ⋯ = ⋯

theorem SeparationQuotient.t2Space_iff {X : Type u_1} [TopologicalSpace X] : T2Space (SeparationQuotient X) ↔ R1Space X

instance SeparationQuotient.t2Space {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space (SeparationQuotient X)

Equations

• ⋯ = ⋯

@[instance 80]

instance instT2SpaceOfR1SpaceOfT0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] [T0Space X] : T2Space X

Equations

• ⋯ = ⋯

theorem R1Space.t2Space_iff_t0Space {X : Type u_1} [TopologicalSpace X] [R1Space X] : T2Space X ↔ T0Space X

theorem t2_iff_nhds {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ ∀ {x y : X}, (nhds x ⊓ nhds y).NeBot → 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 : (nhds x ⊓ nhds y).NeBot) : 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 x → ↑f ≤ nhds y → x = y

theorem t2_iff_isClosed_diagonal {X : Type u_1} [TopologicalSpace X] : T2Space X ↔ IsClosed (Set.diagonal X)

theorem isClosed_diagonal {X : Type u_1} [TopologicalSpace X] [T2Space X] : IsClosed (Set.diagonal X)

theorem tendsto_nhds_unique {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] {f : Y → X} {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 : Y → X} {l : Filter Y} {a : X} {b : X} : l.NeBot → Filter.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 : Y → X} {g : Y → X} {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 : Y → X} {g : Y → X} {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) : nhdsSet (s ∩ t) = nhdsSet s ⊓ nhdsSet 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 : X → Y} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ 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 : X → Y} {s : Set X} (inj : Set.InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ 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.

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 ∈ U → U ∈ ↑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 : Y → X} (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 : Y → X} (h : ∃ (x : X), Filter.Tendsto g f (nhds x)) {x : X} : limUnder f g = x ↔ Filter.Tendsto g f (nhds x)

theorem Continuous.limUnder_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] {f : Y → X} (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:

• separated_by_continuous says that two points x y : X can be separated by open neighborhoods provided that there exists a continuous map f : X → Y with a Hausdorff codomain such that f x ≠ f y. We use this lemma to prove that topological spaces defined using induced are Hausdorff spaces.

• separated_by_openEmbedding says that for an open embedding f : X → Y of a Hausdorff space X, the images of two distinct points x y : X, x ≠ y can be separated by open neighborhoods. We use this lemma to prove that topological spaces defined using coinduced are Hausdorff spaces.

@[instance 100]

instance DiscreteTopology.toT2Space {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : T2Space X

Equations

• ⋯ = ⋯

theorem separated_by_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (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 : X → Y} (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 : X → Prop} [T2Space X] : T2Space (Subtype p)

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 : X → Y} (hinj : Function.Injective f) (hc : Continuous f) : T2Space X

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 : X → Y} (hf : Embedding f) : T2Space X

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

instance ULift.instT2Space {X : Type u_1} [TopologicalSpace X] [T2Space X] : T2Space (ULift.{u_3, u_1} X)

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 : X → Type 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] : Setoid X

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

Equations

• t2Setoid X = sInf {s : Setoid X | T2Space (Quotient s)}

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

• t2Quotient X = Quotient (t2Setoid X)

instance t2Quotient.instTopologicalSpace {X : Type u_1} [TopologicalSpace X] : TopologicalSpace (t2Quotient X)

Equations

• t2Quotient.instTopologicalSpace = inferInstanceAs (TopologicalSpace (Quotient (t2Setoid X)))

def t2Quotient.mk {X : Type u_1} [TopologicalSpace X] : X → t2Quotient X

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

Equations

• t2Quotient.mk = Quotient.mk (t2Setoid X)

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.surjective_mk (X : Type u_1) [TopologicalSpace X] : Function.Surjective t2Quotient.mk

theorem t2Quotient.continuous_mk (X : Type u_1) [TopologicalSpace X] : Continuous t2Quotient.mk

theorem t2Quotient.inductionOn {X : Type u_1} [TopologicalSpace X] {motive : t2Quotient X → Prop} (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 X → t2Quotient Y → Prop} (q : t2Quotient X) (q' : t2Quotient Y) (h : ∀ (x : X) (y : Y), motive (t2Quotient.mk x) (t2Quotient.mk y)) : motive q q'

instance t2Quotient.instT2Space {X : Type u_1} [TopologicalSpace X] : T2Space (t2Quotient X)

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 : X → Y} (hf : Continuous f) (a : X) (b : X) : a ≈ b → f a = f b

def t2Quotient.lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) : t2Quotient X → Y

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

• t2Quotient.lift hf = Quotient.lift f ⋯

theorem t2Quotient.continuous_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) : Continuous (t2Quotient.lift hf)

@[simp]

theorem t2Quotient.lift_mk {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) (x : X) : t2Quotient.lift hf (t2Quotient.mk x) = f x

theorem t2Quotient.unique_lift {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) {g : t2Quotient X → Y} (hfg : g ∘ t2Quotient.mk = f) : g = t2Quotient.lift hf

theorem isClosed_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T2Space X] {f : Y → X} {g : Y → X} (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 : Y → X} {g : Y → X} (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 : Y → X} {g : Y → X} (h : Set.EqOn f g s) (hf : Continuous f) (hg : Continuous g) : Set.EqOn f g (closure s)

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 : Y → X} {g : Y → X} (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 : X → Y → Z} {g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, 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 s → ∀ y ∈ closure 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 : X → Y → Z} {g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y) (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) (x : X) : x ∈ closure s → ∀ y ∈ closure 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 : X → Y} {g : X → Y} (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 : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosed (Set.range 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 : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosed (Set.range 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 : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : ClosedEmbedding 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) : SeparatedNhds 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) : SeparatedNhds 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 : x ∉ s) : 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 : x ∉ s) : 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) : IsClosed 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 : X → Y} {s : Set Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s)

theorem Pi.isCompact_iff {ι : Type u_4} {π : ι → Type u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} : IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (Function.eval i '' s)

theorem Pi.isCompact_closure_iff {ι : Type u_4} {π : ι → Type u_5} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T2Space (π i)] {s : Set ((i : ι) → π i)} : IsCompact (closure s) ↔ ∀ (i : ι), IsCompact (closure (Function.eval i '' s))

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 CompactExhaustion.isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] (K : CompactExhaustion X) (n : ℕ) : IsClosed (K n)

theorem IsCompact.inter {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ 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 : X → Y} (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 : X → Y} (h : Continuous f) : IsClosedMap 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 : X → Y} (h : Continuous f) (hf : Function.Injective f) : ClosedEmbedding 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 : X → Y} (hsurj : Function.Surjective f) (hcont : Continuous f) : QuotientMap f

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

theorem isPreirreducible_iff_subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} : IsPreirreducible S ↔ S.Subsingleton

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}

theorem not_preirreducible_nontrivial_t2 (X : Type u_4) [TopologicalSpace X] [PreirreducibleSpace X] [Nontrivial X] [T2Space X] : False

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 s → a ∉ s → Disjoint (nhdsSet s) (nhds a)

class RegularSpace (X : Type u) [TopologicalSpace X] : Prop

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 s → a ∉ s → Disjoint (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.regular {X : Type u} [TopologicalSpace X] [self : RegularSpace X] {s : Set X} {a : X} : IsClosed s → a ∉ s → Disjoint (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), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds 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) : RegularSpace X

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

Alias of RegularSpace.of_lift'_closure.

theorem RegularSpace.of_hasBasis {X : Type u_1} [TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) : RegularSpace X

@[deprecated RegularSpace.of_hasBasis]

theorem RegularSpace.ofBasis {X : Type u_1} [TopologicalSpace X] {ι : X → Sort u_3} {p : (a : X) → ι a → Prop} {s : (a : X) → ι a → Set X} (h₁ : ∀ (a : X), (nhds a).HasBasis (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) : RegularSpace X

Alias of RegularSpace.of_hasBasis.

theorem RegularSpace.of_exists_mem_nhds_isClosed_subset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s) : RegularSpace X

@[deprecated RegularSpace.of_exists_mem_nhds_isClosed_subset]

theorem RegularSpace.ofExistsMemNhdsIsClosedSubset {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s) : RegularSpace X

Alias of RegularSpace.of_exists_mem_nhds_isClosed_subset.

@[instance 100]

instance instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space {X : Type u_1} [TopologicalSpace X] [WeaklyLocallyCompactSpace X] [R1Space X] : RegularSpace X

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) ↔ x ∉ closure s

theorem disjoint_nhds_nhdsSet {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {x : X} {s : Set X} : Disjoint (nhds x) (nhdsSet s) ↔ x ∉ closure s

@[instance 100]

instance instR1Space {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : R1Space 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) : (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 TopologicalSpace.IsTopologicalBasis.exists_closure_subset {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) {x : X} {s : Set X} (h : s ∈ nhds x) : ∃ t ∈ B, x ∈ t ∧ closure t ⊆ s

theorem Inducing.regularSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] {f : Y → X} (hf : Inducing f) : RegularSpace Y

theorem regularSpace_induced {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] (f : Y → X) : RegularSpace Y

theorem regularSpace_sInf {X : Type u_3} {T : Set (TopologicalSpace X)} (h : ∀ t ∈ T, RegularSpace X) : RegularSpace X

theorem regularSpace_iInf {ι : Sort u_3} {X : Type u_4} {t : ι → TopologicalSpace X} (h : ∀ (i : ι), RegularSpace X) : RegularSpace X

theorem RegularSpace.inf {X : Type u_3} {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} (h₁ : RegularSpace X) (h₂ : RegularSpace X) : RegularSpace X

instance instRegularSpaceSubtype {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {p : X → Prop} : RegularSpace (Subtype p)

Equations

• ⋯ = ⋯

instance instRegularSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [RegularSpace X] [TopologicalSpace Y] [RegularSpace Y] : RegularSpace (X × Y)

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) : SeparatedNhds 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) : SeparatedNhds 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) : HasSeparatingCover 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]

theorem locally_compact_of_compact {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] : LocallyCompactSpace X

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

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 ≠ y → Disjoint ((nhds x).lift' closure) ((nhds y).lift' closure)

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

theorem T25Space.t2_5 {X : Type u} [TopologicalSpace X] [self : T25Space X] ⦃x : X⦄ ⦃y : X⦄ : x ≠ y → Disjoint ((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] : T2Space 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 : X → Y} (hinj : Function.Injective f) (hcont : Continuous f) : T25Space X

instance instT25SpaceSubtype {X : Type u_1} [TopologicalSpace X] [T25Space X] {p : X → Prop} : T25Space { x : X // p x }

Equations

• ⋯ = ⋯

class T3Space (X : Type u) [TopologicalSpace X] extends T0Space , RegularSpace : Prop

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.

@[instance 90]

instance instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] : T3Space X

Equations

• ⋯ = ⋯

theorem RegularSpace.t3Space_iff_t0Space {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : T3Space X ↔ T0Space X

@[instance 100]

instance T3Space.t25Space {X : Type u_1} [TopologicalSpace X] [T3Space X] : T25Space X

Equations

• ⋯ = ⋯

theorem Embedding.t3Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space Y] {f : X → Y} (hf : Embedding f) : T3Space X

instance Subtype.t3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] {p : X → Prop} : T3Space (Subtype p)

Equations

• ⋯ = ⋯

instance ULift.instT3Space {X : Type u_1} [TopologicalSpace X] [T3Space X] : T3Space (ULift.{u_3, u_1} X)

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.

instance instT3SpaceSeparationQuotientOfRegularSpace {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : T3Space (SeparationQuotient X)

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

Equations

• ⋯ = ⋯

class NormalSpace (X : Type u) [TopologicalSpace X] : Prop

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

• normal : ∀ (s t : Set X), IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t

  Two disjoint sets in a normal space admit disjoint neighbourhoods.

theorem NormalSpace.normal {X : Type u} [TopologicalSpace X] [self : NormalSpace X] (s : Set X) (t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds 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) : SeparatedNhds 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) : Disjoint (nhdsSet s) (nhdsSet 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 : X → Y} (hf : ClosedEmbedding f) : NormalSpace X

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

@[instance 100]

instance NormalSpace.of_compactSpace_r1Space {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [R1Space X] : NormalSpace X

Equations

• ⋯ = ⋯

@[instance 100]

instance NormalSpace.of_regularSpace_lindelofSpace {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LindelofSpace X] : NormalSpace X

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

• ⋯ = ⋯

@[instance 100]

instance NormalSpace.of_regularSpace_secondCountableTopology {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : NormalSpace X

Equations

• ⋯ = ⋯

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

A T₄ space is a normal T₁ space.

@[instance 100]

instance instT4SpaceOfT1SpaceOfNormalSpace {X : Type u_1} [TopologicalSpace X] [T1Space X] [NormalSpace X] : T4Space X

Equations

• ⋯ = ⋯

@[instance 100]

instance T4Space.t3Space {X : Type u_1} [TopologicalSpace X] [T4Space X] : T3Space X

Equations

• ⋯ = ⋯

@[deprecated inferInstance]

theorem T4Space.of_compactSpace_t2Space {X : Type u_1} [TopologicalSpace X] [CompactSpace X] [T2Space X] : T4Space X

theorem ClosedEmbedding.t4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T4Space Y] {f : X → Y} (hf : ClosedEmbedding f) : T4Space X

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

instance ULift.instT4Space {X : Type u_1} [TopologicalSpace X] [T4Space X] : T4Space (ULift.{u_3, u_1} X)

Equations

• ⋯ = ⋯

instance SeparationQuotient.instNormalSpace {X : Type u_1} [TopologicalSpace X] [NormalSpace X] : NormalSpace (SeparationQuotient X)

The SeparationQuotient of a normal space is a normal space.

Equations

• ⋯ = ⋯

class CompletelyNormalSpace (X : Type u) [TopologicalSpace X] : Prop

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.

• completely_normal : ∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t)

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

theorem CompletelyNormalSpace.completely_normal {X : Type u} [TopologicalSpace X] [self : CompletelyNormalSpace X] ⦃s : Set X⦄ ⦃t : Set X⦄ : Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (nhdsSet s) (nhdsSet t)

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

@[instance 100]

instance CompletelyNormalSpace.toNormalSpace {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] : NormalSpace X

A completely normal space is a normal space.

Equations

• ⋯ = ⋯

theorem Embedding.completelyNormalSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [CompletelyNormalSpace Y] {e : X → Y} (he : Embedding e) : CompletelyNormalSpace X

instance instCompletelyNormalSpaceSubtype {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] {p : X → Prop} : CompletelyNormalSpace { x : X // p x }

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

Equations

• ⋯ = ⋯

instance ULift.instCompletelyNormalSpace {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] : CompletelyNormalSpace (ULift.{u_3, u_1} X)

Equations

• ⋯ = ⋯

class T5Space (X : Type u) [TopologicalSpace X] extends T1Space , CompletelyNormalSpace : Prop

A T₅ space is a normal T₁ space.

theorem Embedding.t5Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T5Space Y] {e : X → Y} (he : Embedding e) : T5Space X

@[instance 100]

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

A T₅ space is a T₄ space.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

instance ULift.instT5Space {X : Type u_1} [TopologicalSpace X] [T5Space X] : T5Space (ULift.{u_3, u_1} X)

Equations

• ⋯ = ⋯

instance instT5SpaceSeparationQuotientOfCompletelyNormalSpaceOfR0Space {X : Type u_1} [TopologicalSpace X] [CompletelyNormalSpace X] [R0Space X] : T5Space (SeparationQuotient X)

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.

theorem totallySeparatedSpace_of_t1_of_basis_clopen {X : Type u_1} [TopologicalSpace X] [T1Space X] (h : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}) : TotallySeparatedSpace X

A T1 space with a clopen basis is totally separated.

theorem compact_t2_tot_disc_iff_tot_sep {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] : TotallyDisconnectedSpace X ↔ TotallySeparatedSpace X

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]

instance instTotallySeparatedSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] : TotallySeparatedSpace X

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 isTopologicalBasis_isClopen {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [TotallyDisconnectedSpace X] : TopologicalSpace.IsTopologicalBasis {s : Set X | IsClopen s}

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.

theorem loc_compact_Haus_tot_disc_of_zero_dim {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TopologicalSpace.IsTopologicalBasis {s : Set H | IsClopen s}

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

theorem loc_compact_t2_tot_disc_iff_tot_sep {H : Type u_3} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] : TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H

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

instance ConnectedComponents.t2 {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] : T2Space (ConnectedComponents X)

ConnectedComponents X is Hausdorff when X is Hausdorff and compact

Equations

• ⋯ = ⋯