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.
• 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.
• 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.)
• 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.
• 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.
• 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 T0 regular space. In mathlib, T₃ implies T₂.₅.
• NormalSpace: A normal space, is one where given two disjoint closed sets, we can find two open sets that separate them.
• T4Space: A T₄ space is a normal T₁ space. T₄ implies T₃.
• T5Space: A T₅ space, also known as a completely normal Hausdorff space, is a space in which, given two sets s and t such that the closure of s is disjoint from t, and conversely, then s and t have disjoint neighborhoods.

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_open_singleton_of_open_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.
• finset_disjoint_finset_opens_of_t2: 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.

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.

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

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.

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)

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

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_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

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : T0Space (SeparationQuotient X)) = (_ : T0Space (SeparationQuotient X))

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

• (_ : T0Space (Subtype p)) = (_ : T0Space (Subtype p))

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

• (_ : T0Space (X × Y)) = (_ : T0Space (X × Y))

instance Pi.instT0Space {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T0Space (X i)] : T0Space ((i : ι) → X i)

Equations

• (_ : T0Space ((i : ι) → X i)) = (_ : T0Space ((i : ι) → X i))

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

Equations

• (_ : T0Space (ULift.{u_3, u_1} X)) = (_ : T0Space (ULift.{u_3, u_1} X))

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

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 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 : Set.Finite s) : 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 Filter.coclosedCompact_le_cofinite {X : Type u_1} [TopologicalSpace X] [T1Space X] : Filter.coclosedCompact X ≤ Filter.cofinite

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

In a T1Space, 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' := (_ : Filter.coclosedCompact X ≤ Filter.cofinite) }

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

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

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, 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]

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 instT1SpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology {X : Type u_1} : T1Space (CofiniteTopology X)

Equations

• (_ : T1Space (CofiniteTopology X)) = (_ : T1Space (CofiniteTopology X))

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

• (_ : T1Space (Subtype p)) = (_ : T1Space (Subtype p))

instance instT1SpaceProdInstTopologicalSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T1Space X] [T1Space Y] : T1Space (X × Y)

Equations

• (_ : T1Space (X × Y)) = (_ : T1Space (X × Y))

instance instT1SpaceForAllTopologicalSpace {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T1Space (X i)] : T1Space ((i : ι) → X i)

Equations

• (_ : T1Space ((i : ι) → X i)) = (_ : T1Space ((i : ι) → X i))

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

Equations

• (_ : T1Space (ULift.{u_3, u_1} X)) = (_ : T1Space (ULift.{u_3, u_1} X))

instance T1Space.t0Space {X : Type u_1} [TopologicalSpace X] [T1Space X] : T0Space X

Equations

• (_ : T0Space X) = (_ : T0Space X)

@[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 : Set.Subsingleton s) : Set.Subsingleton (closure s)

@[simp]

theorem subsingleton_closure {X : Type u_1} [TopologicalSpace X] [T1Space X] {s : Set X} : Set.Subsingleton (closure s) ↔ Set.Subsingleton s

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) : 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 ↔ 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) [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 : 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} [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) : Set.Infinite s

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 : Set.Nontrivial s) : Set.Infinite s

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

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

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

Equations

• (_ : Filter.NeBot (nhdsWithin x {x}ᶜ)) = (_ : Filter.NeBot (nhdsWithin x {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 : 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.

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 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) : Set.PairwiseDisjoint s nhds

theorem Set.Finite.t2_separation {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : Set.Finite s) : ∃ (U : X → Set 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.

theorem isOpen_setOf_disjoint_nhds_nhds {X : Type u_1} [TopologicalSpace X] : IsOpen {p : X × X | Disjoint (nhds p.1) (nhds p.2)}

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

Equations

• (_ : T1Space X) = (_ : T1Space X)

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 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} [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 : Y → X} {l : Filter Y} {a : X} {b : X} : Filter.NeBot l → 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} [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 : 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 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.

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

instance T25Space.t2Space {X : Type u_1} [TopologicalSpace X] [T25Space X] : T2Space X

Equations

• (_ : T2Space X) = (_ : T2Space X)

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)

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 Ultrafilter.lim_eq_iff_le_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] {x : X} {F : Ultrafilter X} : Ultrafilter.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 ∈ 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} [Filter.NeBot f] {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} [Filter.NeBot f] {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 DiscreteTopology.toT2Space {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] : T2Space X

Equations

• (_ : T2Space X) = (_ : T2Space X)

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

Equations

• (_ : T2Space (Subtype p)) = (_ : T2Space (Subtype p))

instance Prod.t2Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X × Y)

Equations

• (_ : T2Space (X × Y)) = (_ : T2Space (X × Y))

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

• (_ : T2Space (ULift.{u_3, u_1} X)) = (_ : T2Space (ULift.{u_3, u_1} X))

instance instT2SpaceSumInstTopologicalSpaceSum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X ⊕ Y)

Equations

• (_ : T2Space (X ⊕ Y)) = (_ : T2Space (X ⊕ Y))

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

• (_ : T2Space ((a : X) → Y a)) = (_ : T2Space ((a : X) → Y a))

instance Sigma.t2Space {ι : Type u_4} {X : ι → Type u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)] : T2Space ((i : ι) × X i)

Equations

• (_ : T2Space ((i : ι) × X i)) = (_ : T2Space ((i : ι) × X i))

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

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 isCompact_isCompact_separated {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

theorem finset_disjoint_finset_opens_of_t2 {X : Type u_1} [TopologicalSpace X] [T2Space X] (s : Finset X) (t : Finset X) (h : Disjoint s t) : SeparatedNhds ↑s ↑t

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

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.

@[simp]

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

@[simp]

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

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 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 isCompact_closure_of_subset_compact {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (ht : IsCompact t) (h : s ⊆ t) : IsCompact (closure s)

@[simp]

theorem exists_compact_superset_iff {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} : (∃ (K : Set X), IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)

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 IsCompact.binary_compact_cover {X : Type u_1} [TopologicalSpace X] [T2Space 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 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 IsCompact.finite_compact_cover {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} (hs : IsCompact s) {ι : Type u_4} (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ᵢ.

instance instLocallyCompactPair_1 {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [WeaklyLocallyCompactSpace X] [T2Space Y] : LocallyCompactPair X Y

Equations

• (_ : LocallyCompactPair X Y) = (_ : LocallyCompactPair X Y)

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

A weakly locally compact Hausdorff space is locally compact.

Equations

• (_ : LocallyCompactSpace X) = (_ : LocallyCompactSpace X)

@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]

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

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

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

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

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

theorem exists_open_between_and_isCompact_closure {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space 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 T₂ 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.

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

theorem IsPreirreducible.subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] {S : Set X} (h : IsPreirreducible S) : Set.Subsingleton S

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_TFAE (X : Type u) [TopologicalSpace X] : List.TFAE [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), Filter.lift' (nhds x) closure ≤ nhds x, ∀ (x : X), Filter.lift' (nhds x) closure = nhds x]

theorem RegularSpace.ofLift'_closure {X : Type u_1} [TopologicalSpace X] (h : ∀ (x : X), Filter.lift' (nhds x) closure = nhds x) : RegularSpace X

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), Filter.HasBasis (nhds a) (p a) (s a)) (h₂ : ∀ (a : X) (i : ι a), p a i → IsClosed (s a i)) : RegularSpace X

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

instance instRegularSpace {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] : RegularSpace X

A locally compact T2 space is regular.

Equations

• (_ : RegularSpace X) = (_ : RegularSpace X)

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

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 TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {B : Set (Set X)} (hB : TopologicalSpace.IsTopologicalBasis B) (x : X) : Filter.HasBasis (nhds x) (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 disjoint_nhds_nhds_iff_not_specializes {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {a : X} {b : X} : Disjoint (nhds a) (nhds b) ↔ ¬a ⤳ b

theorem specializes_comm {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {a : X} {b : X} : a ⤳ b ↔ b ⤳ a

theorem Specializes.symm {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {a : X} {b : X} : a ⤳ b → b ⤳ a

Alias of the forward direction of specializes_comm.

theorem specializes_iff_inseparable {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {a : X} {b : X} : a ⤳ b ↔ Inseparable a b

theorem isClosed_setOf_specializes {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : IsClosed {p : X × X | p.1 ⤳ p.2}

theorem isClosed_setOf_inseparable {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : IsClosed {p : X × X | Inseparable p.1 p.2}

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 instRegularSpaceSubtypeInstTopologicalSpaceSubtype {X : Type u_1} [TopologicalSpace X] [RegularSpace X] {p : X → Prop} : RegularSpace (Subtype p)

Equations

• (_ : RegularSpace (Subtype p)) = (_ : RegularSpace (Subtype p))

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

Equations

• (_ : RegularSpace (X × Y)) = (_ : RegularSpace (X × Y))

instance instRegularSpaceForAllTopologicalSpace {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), RegularSpace (X i)] : RegularSpace ((i : ι) → X i)

Equations

• (_ : RegularSpace ((i : ι) → X i)) = (_ : RegularSpace ((i : ι) → X i))

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

A class of topological spaces in which, given a compact set included inside an open set, then the closure of the compact set is also included in the open set. Satisfied notably for T2 spaces and regular spaces, and useful when discussing classes of regular measures. Equivalent to regularity among locally compact spaces.

• closure_subset_of_isOpen : ∀ (K U : Set X), IsCompact K → IsOpen U → K ⊆ U → closure K ⊆ U

theorem IsCompact.closure_subset_of_isOpen {X : Type u_1} [TopologicalSpace X] [ClosableCompactSubsetOpenSpace X] {s : Set X} (hs : IsCompact s) {u : Set X} (hu : IsOpen u) (h : s ⊆ u) : closure s ⊆ u

instance instClosableCompactSubsetOpenSpace {X : Type u_1} [TopologicalSpace X] [T2Space X] : ClosableCompactSubsetOpenSpace X

Equations

• (_ : ClosableCompactSubsetOpenSpace X) = (_ : ClosableCompactSubsetOpenSpace X)

instance instClosableCompactSubsetOpenSpace_1 {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : ClosableCompactSubsetOpenSpace X

In a (possibly non-Hausdorff) regular space, if a compact set s is contained in an open set u, then its closure is also contained in u.

Equations

• (_ : ClosableCompactSubsetOpenSpace X) = (_ : ClosableCompactSubsetOpenSpace X)

theorem exists_compact_closed_between {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [ClosableCompactSubsetOpenSpace 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 space with the ClosableCompactSubsetOpenSpace property (for instance regular spaces), 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.

instance instRegularSpace_1 {X : Type u_1} [TopologicalSpace X] [LocallyCompactSpace X] [ClosableCompactSubsetOpenSpace X] : RegularSpace X

A locally compact space with the ClosableCompactSubsetOpenSpace is Regular.

Equations

• (_ : RegularSpace X) = (_ : RegularSpace X)

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

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 instT3Space {X : Type u_1} [TopologicalSpace X] [T0Space X] [RegularSpace X] : T3Space X

Equations

• (_ : T3Space X) = (_ : T3Space X)

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

Equations

• (_ : T25Space X) = (_ : T25Space X)

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

• (_ : T3Space (Subtype p)) = (_ : T3Space (Subtype p))

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

Equations

• (_ : T3Space (ULift.{u_3, u_1} X)) = (_ : T3Space (ULift.{u_3, u_1} X))

instance instT3SpaceProdInstTopologicalSpaceProd {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [T3Space X] [T3Space Y] : T3Space (X × Y)

Equations

• (_ : T3Space (X × Y)) = (_ : T3Space (X × Y))

instance instT3SpaceForAllTopologicalSpace {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)] : T3Space ((i : ι) → X i)

Equations

• (_ : T3Space ((i : ι) → X i)) = (_ : T3Space ((i : ι) → X i))

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 instT3SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient {X : Type u_1} [TopologicalSpace X] [RegularSpace X] : T3Space (SeparationQuotient X)

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

Equations

• (_ : T3Space (SeparationQuotient X)) = (_ : T3Space (SeparationQuotient X))

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 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 NormalSpace.of_regularSpace_secondCountableTopology {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [SecondCountableTopology X] : NormalSpace X

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

Equations

• (_ : NormalSpace X) = (_ : NormalSpace X)

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

A T₄ space is a normal T₁ space.

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

Equations

• (_ : T4Space X) = (_ : T4Space X)

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

Equations

• (_ : T3Space X) = (_ : T3Space X)

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

Equations

• (_ : T4Space 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

• (_ : T4Space (ULift.{u_3, u_1} X)) = (_ : T4Space (ULift.{u_3, u_1} X))

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

The SeparationQuotient of a normal space is a normal space.

Equations

• (_ : NormalSpace (SeparationQuotient X)) = (_ : NormalSpace (SeparationQuotient X))

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

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.

• t1 : ∀ (x : X), IsClosed {x}
• 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 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 instT5SpaceSubtypeInstTopologicalSpaceSubtype {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

• (_ : T5Space { x : X // p x }) = (_ : T5Space { x : X // p x })

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

Equations

• (_ : T5Space (ULift.{u_3, u_1} X)) = (_ : T5Space (ULift.{u_3, u_1} X))

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

A T₅ space is a T₄ space.

Equations

• (_ : T4Space X) = (_ : T4Space X)

instance instT5SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient {X : Type u_1} [TopologicalSpace X] [T5Space X] : T5Space (SeparationQuotient X)

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

• (_ : T5Space (SeparationQuotient X)) = (_ : T5Space (SeparationQuotient X))

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

• (_ : TotallySeparatedSpace X) = (_ : TotallySeparatedSpace X)

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

• (_ : T2Space (ConnectedComponents X)) = (_ : T2Space (ConnectedComponents X))