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.
• T3Space: A T₃ space, is one where given any closed C and x ∉ C, there is disjoint open sets containing x and C respectively. 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

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_finset Given an open Finset 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 α (that is, the set of all points of the form (a, a) : α × α) 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 α 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.
• connected_components_eq_Inter_clopen: 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 α is T₂ for α 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 {α : Type u} [TopologicalSpace α] : Set α → Set α → 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 V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ Disjoint U V

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

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

Alias of the forward direction of separatedNhds_iff_disjoint.

theorem SeparatedNhds.symm {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} : SeparatedNhds s t → SeparatedNhds t s

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

theorem SeparatedNhds.preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} {t : Set β} (h : SeparatedNhds s t) (hf : Continuous f) : SeparatedNhds (f ⁻¹' s) (f ⁻¹' t)

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

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

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

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

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

theorem SeparatedNhds.mono {α : Type u} [TopologicalSpace α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h : SeparatedNhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : SeparatedNhds s₁ t₁

theorem SeparatedNhds.union_left {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} {u : Set α} : SeparatedNhds s u → SeparatedNhds t u → SeparatedNhds (s ∪ t) u

theorem SeparatedNhds.union_right {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} {u : Set α} (ht : SeparatedNhds s t) (hu : SeparatedNhds s u) : SeparatedNhds s (t ∪ u)

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

• t0 : ∀ ⦃x y : α⦄, Inseparable x y → x = y

  Two inseparable points in a T₀ space are equal.

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.

theorem t0Space_iff_inseparable (α : Type u) [TopologicalSpace α] : T0Space α ↔ ∀ (x y : α), Inseparable x y → x = y

theorem t0Space_iff_not_inseparable (α : Type u) [TopologicalSpace α] : T0Space α ↔ ∀ (x y : α), x ≠ y → ¬Inseparable x y

theorem Inseparable.eq {α : Type u} [TopologicalSpace α] [T0Space α] {x : α} {y : α} (h : Inseparable x y) : x = y

theorem Inducing.injective {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T0Space α] {f : α → β} (hf : Inducing f) : Function.Injective f

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

theorem Inducing.embedding {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T0Space α] {f : α → β} (hf : Inducing f) : Embedding f

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

theorem embedding_iff_inducing {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T0Space α] {f : α → β} : Embedding f ↔ Inducing f

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

theorem nhds_injective {α : Type u} [TopologicalSpace α] [T0Space α] : Function.Injective nhds

theorem inseparable_iff_eq {α : Type u} [TopologicalSpace α] [T0Space α] {x : α} {y : α} : Inseparable x y ↔ x = y

@[simp]

theorem nhds_eq_nhds_iff {α : Type u} [TopologicalSpace α] [T0Space α] {a : α} {b : α} : nhds a = nhds b ↔ a = b

@[simp]

theorem inseparable_eq_eq {α : Type u} [TopologicalSpace α] [T0Space α] : Inseparable = Eq

theorem TopologicalSpace.IsTopologicalBasis.inseparable_iff {α : Type u} [TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : α} {y : α} : Inseparable x y ↔ ∀ (s : Set α), s ∈ b → (x ∈ s ↔ y ∈ s)

theorem TopologicalSpace.IsTopologicalBasis.eq_iff {α : Type u} [TopologicalSpace α] [T0Space α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : α} {y : α} : x = y ↔ ∀ (s : Set α), s ∈ b → (x ∈ s ↔ y ∈ s)

theorem t0Space_iff_exists_isOpen_xor'_mem (α : Type u) [TopologicalSpace α] : T0Space α ↔ ∀ (x y : α), x ≠ y → ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

theorem exists_isOpen_xor'_mem {α : Type u} [TopologicalSpace α] [T0Space α] {x : α} {y : α} (h : x ≠ y) : ∃ U, IsOpen U ∧ Xor' (x ∈ U) (y ∈ U)

def specializationOrder (α : Type u_1) [TopologicalSpace α] [T0Space α] : PartialOrder α

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 {α : Type u} [TopologicalSpace α] : T0Space (SeparationQuotient α)

Equations

• @instT0SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient = @instT0SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient.proof_1

theorem minimal_nonempty_closed_subsingleton {α : Type u} [TopologicalSpace α] [T0Space α] {s : Set α} (hs : IsClosed s) (hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsClosed t → t = s) : Set.Subsingleton s

theorem minimal_nonempty_closed_eq_singleton {α : Type u} [TopologicalSpace α] [T0Space α] {s : Set α} (hs : IsClosed s) (hne : Set.Nonempty s) (hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsClosed t → t = s) : ∃ x, s = {x}

theorem IsClosed.exists_closed_singleton {α : Type u_1} [TopologicalSpace α] [T0Space α] [CompactSpace α] {S : Set α} (hS : IsClosed S) (hne : Set.Nonempty S) : ∃ x, 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 {α : Type u} [TopologicalSpace α] [T0Space α] {s : Set α} (hs : IsOpen s) (hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s) : Set.Subsingleton s

theorem minimal_nonempty_open_eq_singleton {α : Type u} [TopologicalSpace α] [T0Space α] {s : Set α} (hs : IsOpen s) (hne : Set.Nonempty s) (hmin : ∀ (t : Set α), t ⊆ s → Set.Nonempty t → IsOpen t → t = s) : ∃ x, s = {x}

theorem exists_open_singleton_of_open_finite {α : Type u} [TopologicalSpace α] [T0Space α] {s : Set α} (hfin : Set.Finite s) (hne : Set.Nonempty s) (ho : IsOpen s) : ∃ x, 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 {α : Type u} [TopologicalSpace α] [T0Space α] [Finite α] [Nonempty α] : ∃ x, IsOpen {x}

theorem t0Space_of_injective_of_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Function.Injective f) (hf' : Continuous f) [T0Space β] : T0Space α

theorem Embedding.t0Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T0Space β] {f : α → β} (hf : Embedding f) : T0Space α

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

Equations

• @Subtype.t0Space = @Subtype.t0Space.proof_1

theorem t0Space_iff_or_not_mem_closure (α : Type u) [TopologicalSpace α] : T0Space α ↔ ∀ (a b : α), a ≠ b → ¬a ∈ closure {b} ∨ ¬b ∈ closure {a}

instance Prod.instT0Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T0Space α] [T0Space β] : T0Space (α × β)

Equations

• @Prod.instT0Space = @Prod.instT0Space.proof_1

instance Pi.instT0Space {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T0Space (π i)] : T0Space ((i : ι) → π i)

Equations

• @Pi.instT0Space = @Pi.instT0Space.proof_1

theorem T0Space.of_cover {α : Type u} [TopologicalSpace α] (h : ∀ (x y : α), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s) : T0Space α

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

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

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

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

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.

theorem isClosed_singleton {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} : IsClosed {x}

theorem isOpen_compl_singleton {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} : IsOpen {x}ᶜ

theorem isOpen_ne {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} : IsOpen {y | y ≠ x}

theorem Continuous.isOpen_support {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] [Zero α] [TopologicalSpace β] {f : β → α} (hf : Continuous f) : IsOpen (Function.support f)

theorem Continuous.isOpen_mulSupport {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] [One α] [TopologicalSpace β] {f : β → α} (hf : Continuous f) : IsOpen (Function.mulSupport f)

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

theorem Ne.nhdsWithin_diff_singleton {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} (h : x ≠ y) (s : Set α) : nhdsWithin x (s \ {y}) = nhdsWithin x s

theorem nhdsWithin_compl_singleton_le {α : Type u} [TopologicalSpace α] [T1Space α] (x : α) (y : α) : nhdsWithin x {x}ᶜ ≤ nhdsWithin x {y}ᶜ

theorem isOpen_setOf_eventually_nhdsWithin {α : Type u} [TopologicalSpace α] [T1Space α] {p : α → Prop} : IsOpen {x | ∀ᶠ (y : α) in nhdsWithin x {x}ᶜ, p y}

theorem Set.Finite.isClosed {α : Type u} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Set.Finite s) : IsClosed s

theorem TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne {α : Type u} [TopologicalSpace α] [T1Space α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {x : α} {y : α} (h : x ≠ y) : ∃ a, a ∈ b ∧ x ∈ a ∧ ¬y ∈ a

theorem Filter.coclosedCompact_le_cofinite {α : Type u} [TopologicalSpace α] [T1Space α] : Filter.coclosedCompact α ≤ Filter.cofinite

def Bornology.relativelyCompact (α : Type u) [TopologicalSpace α] [T1Space α] : Bornology α

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 α = { cobounded' := Filter.coclosedCompact α, le_cofinite' := (_ : Filter.coclosedCompact α ≤ Filter.cofinite) }

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

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

theorem t1Space_TFAE (α : Type u) [TopologicalSpace α] : List.TFAE [T1Space α, ∀ (x : α), IsClosed {x}, ∀ (x : α), IsOpen {x}ᶜ, Continuous ↑CofiniteTopology.of, ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : α⦄, x ≠ y → ∃ s, s ∈ nhds x ∧ ¬y ∈ s, ∀ ⦃x y : α⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U, ∀ ⦃x y : α⦄, x ≠ y → Disjoint (nhds x) (pure y), ∀ ⦃x y : α⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : α⦄, x ⤳ y → x = y]

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

theorem CofiniteTopology.continuous_of {α : Type u} [TopologicalSpace α] [T1Space α] : Continuous ↑CofiniteTopology.of

theorem t1Space_iff_exists_open {α : Type u} [TopologicalSpace α] : T1Space α ↔ ∀ (x y : α), x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ ¬y ∈ U

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

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

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

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

theorem disjoint_nhds_pure {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} (h : x ≠ y) : Disjoint (nhds x) (pure y)

theorem Specializes.eq {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} (h : x ⤳ y) : x = y

theorem specializes_iff_eq {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} : x ⤳ y ↔ x = y

@[simp]

theorem specializes_eq_eq {α : Type u} [TopologicalSpace α] [T1Space α] : (fun x x_1 => x ⤳ x_1) = Eq

@[simp]

theorem pure_le_nhds_iff {α : Type u} [TopologicalSpace α] [T1Space α] {a : α} {b : α} : pure a ≤ nhds b ↔ a = b

@[simp]

theorem nhds_le_nhds_iff {α : Type u} [TopologicalSpace α] [T1Space α] {a : α} {b : α} : nhds a ≤ nhds b ↔ a = b

instance instT1SpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology {α : Type u_1} : T1Space (CofiniteTopology α)

Equations

• @instT1SpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology = @instT1SpaceCofiniteTopologyInstTopologicalSpaceCofiniteTopology.proof_1

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

theorem continuousWithinAt_update_of_ne {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] [DecidableEq α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {y : α} {z : β} (hne : y ≠ x) : ContinuousWithinAt (Function.update f x z) s y ↔ ContinuousWithinAt f s y

theorem continuousAt_update_of_ne {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] [DecidableEq α] [TopologicalSpace β] {f : α → β} {x : α} {y : α} {z : β} (hne : y ≠ x) : ContinuousAt (Function.update f x z) y ↔ ContinuousAt f y

theorem continuousOn_update_iff {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] [DecidableEq α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Function.Injective f) (hf' : Continuous f) [T1Space β] : T1Space α

theorem Embedding.t1Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] {f : α → β} (hf : Embedding f) : T1Space α

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

Equations

• @Subtype.t1Space = @Subtype.t1Space.proof_1

instance instT1SpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T1Space α] [T1Space β] : T1Space (α × β)

Equations

• @instT1SpaceProdInstTopologicalSpaceProd = @instT1SpaceProdInstTopologicalSpaceProd.proof_1

instance instT1SpaceForAllTopologicalSpace {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T1Space (π i)] : T1Space ((i : ι) → π i)

Equations

• @instT1SpaceForAllTopologicalSpace = @instT1SpaceForAllTopologicalSpace.proof_1

instance T1Space.t0Space {α : Type u} [TopologicalSpace α] [T1Space α] : T0Space α

Equations

• @T1Space.t0Space = @T1Space.t0Space.proof_1

@[simp]

theorem compl_singleton_mem_nhds_iff {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} : {x}ᶜ ∈ nhds y ↔ y ≠ x

theorem compl_singleton_mem_nhds {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} (h : y ≠ x) : {x}ᶜ ∈ nhds y

@[simp]

theorem closure_singleton {α : Type u} [TopologicalSpace α] [T1Space α] {a : α} : closure {a} = {a}

theorem Set.Subsingleton.closure {α : Type u} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Set.Subsingleton s) : Set.Subsingleton (closure s)

@[simp]

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

theorem isClosedMap_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] {y : β} : IsClosedMap (Function.const α y)

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

theorem insert_mem_nhdsWithin_of_subset_insert {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {y : α} {s : Set α} {t : Set α} (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 {α : Type u} [TopologicalSpace α] [T1Space α] (x : α) : Filter.ker (nhds x) = {x}

theorem biInter_basis_nhds {α : Type u} [TopologicalSpace α] [T1Space α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set α} {x : α} (h : Filter.HasBasis (nhds x) p s) : ⋂ (i : ι) (x : p i), s i = {x}

@[simp]

theorem compl_singleton_mem_nhdsSet_iff {α : Type u} [TopologicalSpace α] [T1Space α] {x : α} {s : Set α} : {x}ᶜ ∈ nhdsSet s ↔ ¬x ∈ s

@[simp]

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

@[simp]

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

theorem injective_nhdsSet {α : Type u} [TopologicalSpace α] [T1Space α] : Function.Injective nhdsSet

theorem strictMono_nhdsSet {α : Type u} [TopologicalSpace α] [T1Space α] : StrictMono nhdsSet

@[simp]

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

theorem Dense.diff_singleton {α : Type u} [TopologicalSpace α] [T1Space α] {s : Set α} (hs : Dense s) (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 {α : Type u} [TopologicalSpace α] [T1Space α] [∀ (x : α), Filter.NeBot (nhdsWithin x {x}ᶜ)] {s : Set α} (hs : Dense s) (t : Finset α) : 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 {α : Type u} [TopologicalSpace α] [T1Space α] [∀ (x : α), Filter.NeBot (nhdsWithin x {x}ᶜ)] {s : Set α} (hs : Dense s) {t : Set α} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] {f : α → β} {a : α} {b : β} (h : Filter.Tendsto f (nhds a) (nhds b)) : f a = b

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

theorem Filter.Tendsto.eventually_ne {β : Type v} [TopologicalSpace β] [T1Space β] {α : Type u_1} {g : α → β} {l : Filter α} {b₁ : β} {b₂ : β} (hg : Filter.Tendsto g l (nhds b₁)) (hb : b₁ ≠ b₂) : ∀ᶠ (z : α) in l, g z ≠ b₂

theorem ContinuousAt.eventually_ne {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] {g : α → β} {a : α} {b : β} (hg1 : ContinuousAt g a) (hg2 : g a ≠ b) : ∀ᶠ (z : α) in nhds a, g z ≠ b

theorem eventually_ne_nhds {α : Type u} [TopologicalSpace α] [T1Space α] {a : α} {b : α} (h : a ≠ b) : ∀ᶠ (x : α) in nhds a, x ≠ b

theorem eventually_ne_nhdsWithin {α : Type u} [TopologicalSpace α] [T1Space α] {a : α} {b : α} {s : Set α} (h : a ≠ b) : ∀ᶠ (x : α) in nhdsWithin a s, x ≠ b

theorem continuousAt_of_tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T1Space β] {f : α → β} {a : α} {b : β} (h : Filter.Tendsto f (nhds a) (nhds b)) : ContinuousAt f a

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

@[simp]

theorem tendsto_const_nhds_iff {α : Type u} {β : Type v} [TopologicalSpace α] [T1Space α] {l : Filter β} [Filter.NeBot l] {c : α} {d : α} : Filter.Tendsto (fun x => c) l (nhds d) ↔ c = d

theorem isOpen_singleton_of_finite_mem_nhds {α : Type u_1} [TopologicalSpace α] [T1Space α] (x : α) {s : Set α} (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 {α : Type u_1} [TopologicalSpace α] [T1Space α] (x : α) [hx : Filter.NeBot (nhdsWithin x {x}ᶜ)] {s : Set α} (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 {α : Type u} [TopologicalSpace α] [PreconnectedSpace α] [DiscreteTopology α] : Subsingleton α

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

theorem ConnectedSpace.infinite {α : Type u} [TopologicalSpace α] [ConnectedSpace α] [Nontrivial α] [T1Space α] : Infinite α

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

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

Equations

• @ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space = @ConnectedSpace.neBot_nhdsWithin_compl_of_nontrivial_of_t1space.proof_1

theorem singleton_mem_nhdsWithin_of_mem_discrete {α : Type u} [TopologicalSpace α] {s : Set α} [DiscreteTopology ↑s] {x : α} (hx : x ∈ s) : {x} ∈ nhdsWithin x s

theorem nhdsWithin_of_mem_discrete {α : Type u} [TopologicalSpace α] {s : Set α} [DiscreteTopology ↑s] {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 {α : Type u} [TopologicalSpace α] {ι : Type u_1} {p : ι → Prop} {t : ι → Set α} {s : Set α} [DiscreteTopology ↑s] {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 {α : Type u} [TopologicalSpace α] {s : Set α} [DiscreteTopology ↑s] {x : α} (hx : x ∈ s) : ∃ U, 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 disjoint_nhdsWithin_of_mem_discrete {α : Type u} [TopologicalSpace α] {s : Set α} [DiscreteTopology ↑s] {x : α} (hx : x ∈ s) : ∃ U, 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 (α : Type u) [TopologicalSpace α] : T2Space α ↔ ∀ (x y : α), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

class T2Space (α : Type u) [TopologicalSpace α] : Prop

• t2 : ∀ (x y : α), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

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

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.

theorem t2_separation {α : Type u} [TopologicalSpace α] [T2Space α] {x : α} {y : α} (h : x ≠ y) : ∃ u v, 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 {α : Type u} [TopologicalSpace α] : T2Space α ↔ ∀ (x y : α), x ≠ y → Disjoint (nhds x) (nhds y)

@[simp]

theorem disjoint_nhds_nhds {α : Type u} [TopologicalSpace α] [T2Space α] {x : α} {y : α} : Disjoint (nhds x) (nhds y) ↔ x ≠ y

theorem pairwise_disjoint_nhds {α : Type u} [TopologicalSpace α] [T2Space α] : Pairwise (Disjoint on nhds)

theorem Set.pairwiseDisjoint_nhds {α : Type u} [TopologicalSpace α] [T2Space α] (s : Set α) : Set.PairwiseDisjoint s nhds

theorem Set.Finite.t2_separation {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} (hs : Set.Finite s) : ∃ U, (∀ (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 {α : Type u} [TopologicalSpace α] : IsOpen {p | Disjoint (nhds p.fst) (nhds p.snd)}

instance T2Space.t1Space {α : Type u} [TopologicalSpace α] [T2Space α] : T1Space α

Equations

• @T2Space.t1Space = @T2Space.t1Space.proof_1

theorem t2_iff_nhds {α : Type u} [TopologicalSpace α] : T2Space α ↔ ∀ {x y : α}, 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 {α : Type u} [TopologicalSpace α] [T2Space α] {x : α} {y : α} (h : Filter.NeBot (nhds x ⊓ nhds y)) : x = y

theorem t2Space_iff_nhds {α : Type u} [TopologicalSpace α] : T2Space α ↔ ∀ {x y : α}, x ≠ y → ∃ U, U ∈ nhds x ∧ ∃ V, V ∈ nhds y ∧ Disjoint U V

theorem t2_separation_nhds {α : Type u} [TopologicalSpace α] [T2Space α] {x : α} {y : α} (h : x ≠ y) : ∃ u v, u ∈ nhds x ∧ v ∈ nhds y ∧ Disjoint u v

theorem t2_separation_compact_nhds {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [T2Space α] {x : α} {y : α} (h : x ≠ y) : ∃ u v, u ∈ nhds x ∧ v ∈ nhds y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

theorem t2_iff_ultrafilter {α : Type u} [TopologicalSpace α] : T2Space α ↔ ∀ {x y : α} (f : Ultrafilter α), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y

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

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

theorem tendsto_nhds_unique {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {f : β → α} {l : Filter β} {a : α} {b : α} [Filter.NeBot l] (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto f l (nhds b)) : a = b

theorem tendsto_nhds_unique' {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {f : β → α} {l : Filter β} {a : α} {b : α} : Filter.NeBot l → Filter.Tendsto f l (nhds a) → Filter.Tendsto f l (nhds b) → a = b

theorem tendsto_nhds_unique_of_eventuallyEq {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {f : β → α} {g : β → α} {l : Filter β} {a : α} {b : α} [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 {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {f : β → α} {g : β → α} {l : Filter β} {a : α} {b : α} (ha : Filter.Tendsto f l (nhds a)) (hb : Filter.Tendsto g l (nhds b)) (hfg : ∃ᶠ (x : β) in l, f x = g x) : a = b

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

• t2_5 : ∀ ⦃x y : α⦄, 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.

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 .

@[simp]

theorem disjoint_lift'_closure_nhds {α : Type u} [TopologicalSpace α] [T25Space α] {x : α} {y : α} : Disjoint (Filter.lift' (nhds x) closure) (Filter.lift' (nhds y) closure) ↔ x ≠ y

instance T25Space.t2Space {α : Type u} [TopologicalSpace α] [T25Space α] : T2Space α

Equations

• @T25Space.t2Space = @T25Space.t2Space.proof_1

theorem exists_nhds_disjoint_closure {α : Type u} [TopologicalSpace α] [T25Space α] {x : α} {y : α} (h : x ≠ y) : ∃ s, s ∈ nhds x ∧ ∃ t, t ∈ nhds y ∧ Disjoint (closure s) (closure t)

theorem exists_open_nhds_disjoint_closure {α : Type u} [TopologicalSpace α] [T25Space α] {x : α} {y : α} (h : x ≠ y) : ∃ u, x ∈ u ∧ IsOpen u ∧ ∃ v, y ∈ v ∧ IsOpen v ∧ Disjoint (closure u) (closure v)

Properties of lim and limUnder

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

theorem lim_eq {α : Type u} [TopologicalSpace α] [T2Space α] {f : Filter α} {a : α} [Filter.NeBot f] (h : f ≤ nhds a) : lim f = a

theorem lim_eq_iff {α : Type u} [TopologicalSpace α] [T2Space α] {f : Filter α} [Filter.NeBot f] (h : ∃ a, f ≤ nhds a) {a : α} : lim f = a ↔ f ≤ nhds a

theorem Ultrafilter.lim_eq_iff_le_nhds {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] {x : α} {F : Ultrafilter α} : Ultrafilter.lim F = x ↔ ↑F ≤ nhds x

theorem isOpen_iff_ultrafilter' {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] (U : Set α) : IsOpen U ↔ ∀ (F : Ultrafilter α), Ultrafilter.lim F ∈ U → U ∈ ↑F

theorem Filter.Tendsto.limUnder_eq {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {a : α} {f : Filter β} [Filter.NeBot f] {g : β → α} (h : Filter.Tendsto g f (nhds a)) : limUnder f g = a

theorem Filter.limUnder_eq_iff {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] {f : Filter β} [Filter.NeBot f] {g : β → α} (h : ∃ a, Filter.Tendsto g f (nhds a)) {a : α} : limUnder f g = a ↔ Filter.Tendsto g f (nhds a)

theorem Continuous.limUnder_eq {α : Type u} {β : Type v} [TopologicalSpace α] [T2Space α] [TopologicalSpace β] {f : β → α} (h : Continuous f) (a : β) : limUnder (nhds a) f = f a

@[simp]

theorem lim_nhds {α : Type u} [TopologicalSpace α] [T2Space α] (a : α) : lim (nhds a) = a

@[simp]

theorem limUnder_nhds_id {α : Type u} [TopologicalSpace α] [T2Space α] (a : α) : limUnder (nhds a) id = a

@[simp]

theorem lim_nhdsWithin {α : Type u} [TopologicalSpace α] [T2Space α] {a : α} {s : Set α} (h : a ∈ closure s) : lim (nhdsWithin a s) = a

@[simp]

theorem limUnder_nhdsWithin_id {α : Type u} [TopologicalSpace α] [T2Space α] {a : α} {s : Set α} (h : a ∈ closure s) : limUnder (nhdsWithin a s) id = a

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 : α can be separated by open neighborhoods provided that there exists a continuous map f : α → β 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 : α → β of a Hausdorff space α, the images of two distinct points x y : α, 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 {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : T2Space α

Equations

• @DiscreteTopology.toT2Space = @DiscreteTopology.toT2Space.proof_1

theorem separated_by_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {f : α → β} (hf : Continuous f) {x : α} {y : α} (h : f x ≠ f y) : ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

theorem separated_by_openEmbedding {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {f : α → β} (hf : OpenEmbedding f) {x : α} {y : α} (h : x ≠ y) : ∃ u v, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v

instance instT2SpaceSubtypeInstTopologicalSpaceSubtype {α : Type u_1} {p : α → Prop} [TopologicalSpace α] [T2Space α] : T2Space (Subtype p)

Equations

• @instT2SpaceSubtypeInstTopologicalSpaceSubtype = @instT2SpaceSubtypeInstTopologicalSpaceSubtype.proof_1

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

Equations

• @Prod.t2Space = @Prod.t2Space.proof_1

theorem T2Space.of_injective_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {f : α → β} (hinj : Function.Injective f) (hc : Continuous f) : T2Space α

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

theorem Embedding.t2Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {f : α → β} (hf : Embedding f) : T2Space α

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

instance instT2SpaceSumInstTopologicalSpaceSum {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [T2Space α] [TopologicalSpace β] [T2Space β] : T2Space (α ⊕ β)

Equations

• @instT2SpaceSumInstTopologicalSpaceSum = @instT2SpaceSumInstTopologicalSpaceSum.proof_1

instance Pi.t2Space {α : Type u_1} {β : α → Type v} [(a : α) → TopologicalSpace (β a)] [∀ (a : α), T2Space (β a)] : T2Space ((a : α) → β a)

Equations

• @Pi.t2Space = @Pi.t2Space.proof_1

instance Sigma.t2Space {ι : Type u_2} {α : ι → Type u_1} [(i : ι) → TopologicalSpace (α i)] [∀ (a : ι), T2Space (α a)] : T2Space ((i : ι) × α i)

Equations

• @Sigma.t2Space = @Sigma.t2Space.proof_1

theorem isClosed_eq {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) : IsClosed {x | f x = g x}

theorem isOpen_ne_fun {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) : IsOpen {x | f x ≠ g x}

theorem Set.EqOn.closure {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {s : Set β} {f : β → α} {g : β → α} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {s : Set β} (hs : Dense s) {f : β → α} {g : β → α} (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₂' {α : Type u} {β : Type v} [TopologicalSpace α] {γ : Type u_1} [TopologicalSpace β] [TopologicalSpace γ] [T2Space α] {s : Set β} {t : Set γ} {f : β → γ → α} {g : β → γ → α} (h : ∀ (x : β), x ∈ s → ∀ (y : γ), y ∈ t → f x y = g x y) (hf₁ : ∀ (x : β), Continuous (f x)) (hf₂ : ∀ (y : γ), Continuous fun x => f x y) (hg₁ : ∀ (x : β), Continuous (g x)) (hg₂ : ∀ (y : γ), Continuous fun x => g x y) (x : β) : x ∈ closure s → ∀ (y : γ), y ∈ closure t → f x y = g x y

theorem eqOn_closure₂ {α : Type u} {β : Type v} [TopologicalSpace α] {γ : Type u_1} [TopologicalSpace β] [TopologicalSpace γ] [T2Space α] {s : Set β} {t : Set γ} {f : β → γ → α} {g : β → γ → α} (h : ∀ (x : β), x ∈ s → ∀ (y : γ), y ∈ t → f x y = g x y) (hf : Continuous (Function.uncurry f)) (hg : Continuous (Function.uncurry g)) (x : β) : x ∈ closure s → ∀ (y : γ), y ∈ closure t → f x y = g x y

theorem Set.EqOn.of_subset_closure {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {s : Set β} {t : Set β} {f : β → α} {g : β → α} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosed (Set.range g)

theorem Function.LeftInverse.closedEmbedding {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space α] {f : α → β} {g : β → α} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : ClosedEmbedding g

theorem isCompact_isCompact_separated {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t

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

theorem point_disjoint_finset_opens_of_t2 {α : Type u} [TopologicalSpace α] [T2Space α] {x : α} {s : Finset α} (h : ¬x ∈ s) : SeparatedNhds {x} ↑s

theorem IsCompact.isClosed {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} (hs : IsCompact s) : IsClosed s

In a T2Space, every compact set is closed.

@[simp]

theorem Filter.coclosedCompact_eq_cocompact {α : Type u} [TopologicalSpace α] [T2Space α] : Filter.coclosedCompact α = Filter.cocompact α

@[simp]

theorem Bornology.relativelyCompact_eq_inCompact {α : Type u} [TopologicalSpace α] [T2Space α] : Bornology.relativelyCompact α = Bornology.inCompact α

theorem IsCompact.preimage_continuous {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α → β} {s : Set β} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s)

theorem exists_subset_nhds_of_isCompact {α : Type u} [TopologicalSpace α] [T2Space α] {ι : Type u_2} [Nonempty ι] {V : ι → Set α} (hV : Directed (fun x x_1 => x ⊇ x_1) V) (hV_cpct : ∀ (i : ι), IsCompact (V i)) {U : Set α} (hU : ∀ (x : α), x ∈ ⋂ (i : ι), V i → U ∈ nhds x) : ∃ i, V i ⊆ U

If V : ι → Set α 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 α is assumed to be Hausdorff.

theorem CompactExhaustion.isClosed {α : Type u} [TopologicalSpace α] [T2Space α] (K : CompactExhaustion α) (n : ℕ) : IsClosed (↑K n)

theorem IsCompact.inter {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} {t : Set α} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ t)

theorem isCompact_closure_of_subset_compact {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} {t : Set α} (ht : IsCompact t) (h : s ⊆ t) : IsCompact (closure s)

@[simp]

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

theorem image_closure_of_isCompact {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T2Space β] {s : Set α} (hs : IsCompact (closure s)) {f : α → β} (hf : ContinuousOn f (closure s)) : f '' closure s = closure (f '' s)

theorem IsCompact.binary_compact_cover {α : Type u} [TopologicalSpace α] [T2Space α] {K : Set α} {U : Set α} {V : Set α} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) : ∃ K₁ K₂, 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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α → β} (h : Continuous f) : IsClosedMap f

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

theorem Continuous.closedEmbedding {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α → β} (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 {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [CompactSpace α] [T2Space β] {f : α → β} (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 {α : Type u} [TopologicalSpace α] [T2Space α] {s : Set α} (hs : IsCompact s) {ι : Type u_2} (t : Finset ι) (U : ι → Set α) (hU : ∀ (i : ι), i ∈ t → IsOpen (U i)) (hsC : s ⊆ ⋃ (i : ι) (_ : i ∈ t), U i) : ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι) (_ : i ∈ t), K i

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

instance WeaklyLocallyCompactSpace.locallyCompactSpace {α : Type u} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [T2Space α] : LocallyCompactSpace α

A weakly locally compact Hausdorff space is locally compact.

Equations

• @WeaklyLocallyCompactSpace.locallyCompactSpace = @WeaklyLocallyCompactSpace.locallyCompactSpace.proof_1

@[deprecated WeaklyLocallyCompactSpace.locallyCompactSpace]

theorem locally_compact_of_compact {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] : LocallyCompactSpace α

theorem exists_open_superset_and_isCompact_closure {α : Type u} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [T2Space α] {K : Set α} (hK : IsCompact K) : ∃ V, 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 {α : Type u} [TopologicalSpace α] [WeaklyLocallyCompactSpace α] [T2Space α] (x : α) : ∃ U, 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 {α : Type u} [TopologicalSpace α] [LocallyCompactSpace α] [T2Space α] {K : Set α} {U : Set α} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V, 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 {α : Type u} [TopologicalSpace α] [T2Space α] {S : Set α} : IsPreirreducible S ↔ Set.Subsingleton S

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

theorem isIrreducible_iff_singleton {α : Type u} [TopologicalSpace α] [T2Space α] {S : Set α} : IsIrreducible S ↔ ∃ x, S = {x}

theorem not_preirreducible_nontrivial_t2 (α : Type u_2) [TopologicalSpace α] [PreirreducibleSpace α] [Nontrivial α] [T2Space α] : 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

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

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.

theorem regularSpace_TFAE (X : Type u) [TopologicalSpace X] : List.TFAE [RegularSpace X, ∀ (s : Set X) (a : X), ¬a ∈ closure s → Disjoint (nhdsSet s) (nhds a), ∀ (a : X) (s : Set X), Disjoint (nhdsSet s) (nhds a) ↔ ¬a ∈ closure s, ∀ (a : X) (s : Set X), s ∈ nhds a → ∃ t, t ∈ nhds a ∧ IsClosed t ∧ t ⊆ s, ∀ (a : X), Filter.lift' (nhds a) closure ≤ nhds a, ∀ (a : X), Filter.lift' (nhds a) closure = nhds a]

theorem RegularSpace.ofLift'_closure {α : Type u} [TopologicalSpace α] (h : ∀ (a : α), Filter.lift' (nhds a) closure = nhds a) : RegularSpace α

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

theorem RegularSpace.ofExistsMemNhdsIsClosedSubset {α : Type u} [TopologicalSpace α] (h : ∀ (a : α) (s : Set α), s ∈ nhds a → ∃ t, t ∈ nhds a ∧ IsClosed t ∧ t ⊆ s) : RegularSpace α

theorem disjoint_nhdsSet_nhds {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {s : Set α} : Disjoint (nhdsSet s) (nhds a) ↔ ¬a ∈ closure s

theorem disjoint_nhds_nhdsSet {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {s : Set α} : Disjoint (nhds a) (nhdsSet s) ↔ ¬a ∈ closure s

theorem exists_mem_nhds_isClosed_subset {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {s : Set α} (h : s ∈ nhds a) : ∃ t, t ∈ nhds a ∧ IsClosed t ∧ t ⊆ s

theorem closed_nhds_basis {α : Type u} [TopologicalSpace α] [RegularSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => s ∈ nhds a ∧ IsClosed s) id

theorem lift'_nhds_closure {α : Type u} [TopologicalSpace α] [RegularSpace α] (a : α) : Filter.lift' (nhds a) closure = nhds a

theorem Filter.HasBasis.nhds_closure {α : Type u} [TopologicalSpace α] [RegularSpace α] {ι : Sort u_1} {a : α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis (nhds a) p s) : Filter.HasBasis (nhds a) p fun i => closure (s i)

theorem hasBasis_nhds_closure {α : Type u} [TopologicalSpace α] [RegularSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => s ∈ nhds a) closure

theorem hasBasis_opens_closure {α : Type u} [TopologicalSpace α] [RegularSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => a ∈ s ∧ IsOpen s) closure

theorem TopologicalSpace.IsTopologicalBasis.nhds_basis_closure {α : Type u} [TopologicalSpace α] [RegularSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) (a : α) : Filter.HasBasis (nhds a) (fun s => a ∈ s ∧ s ∈ B) closure

theorem TopologicalSpace.IsTopologicalBasis.exists_closure_subset {α : Type u} [TopologicalSpace α] [RegularSpace α] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {a : α} {s : Set α} (h : s ∈ nhds a) : ∃ t, t ∈ B ∧ a ∈ t ∧ closure t ⊆ s

theorem disjoint_nhds_nhds_iff_not_specializes {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {b : α} : Disjoint (nhds a) (nhds b) ↔ ¬a ⤳ b

theorem specializes_comm {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {b : α} : a ⤳ b ↔ b ⤳ a

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

Alias of the forward direction of specializes_comm.

theorem specializes_iff_inseparable {α : Type u} [TopologicalSpace α] [RegularSpace α] {a : α} {b : α} : a ⤳ b ↔ Inseparable a b

theorem isClosed_setOf_specializes {α : Type u} [TopologicalSpace α] [RegularSpace α] : IsClosed {p | p.fst ⤳ p.snd}

theorem isClosed_setOf_inseparable {α : Type u} [TopologicalSpace α] [RegularSpace α] : IsClosed {p | Inseparable p.fst p.snd}

theorem Inducing.regularSpace {α : Type u} {β : Type v} [TopologicalSpace α] [RegularSpace α] [TopologicalSpace β] {f : β → α} (hf : Inducing f) : RegularSpace β

theorem regularSpace_induced {α : Type u} {β : Type v} [TopologicalSpace α] [RegularSpace α] (f : β → α) : RegularSpace β

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

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

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

instance instRegularSpaceSubtypeInstTopologicalSpaceSubtype {α : Type u} [TopologicalSpace α] [RegularSpace α] {p : α → Prop} : RegularSpace (Subtype p)

Equations

• @instRegularSpaceSubtypeInstTopologicalSpaceSubtype = @instRegularSpaceSubtypeInstTopologicalSpaceSubtype.proof_1

instance instRegularSpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [RegularSpace α] [TopologicalSpace β] [RegularSpace β] : RegularSpace (α × β)

Equations

• @instRegularSpaceProdInstTopologicalSpaceProd = @instRegularSpaceProdInstTopologicalSpaceProd.proof_1

instance instRegularSpaceForAllTopologicalSpace {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), RegularSpace (π i)] : RegularSpace ((i : ι) → π i)

Equations

• @instRegularSpaceForAllTopologicalSpace = @instRegularSpaceForAllTopologicalSpace.proof_1

class T3Space (α : Type u) [TopologicalSpace α] 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 {α : Type u} [TopologicalSpace α] [T0Space α] [RegularSpace α] : T3Space α

Equations

• (_ : T3Space α) = (_ : T3Space α)

instance T3Space.t25Space {α : Type u} [TopologicalSpace α] [T3Space α] : T25Space α

Equations

• @T3Space.t25Space = @T3Space.t25Space.proof_1

theorem Embedding.t3Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T3Space β] {f : α → β} (hf : Embedding f) : T3Space α

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

Equations

• @Subtype.t3Space = @Subtype.t3Space.proof_1

instance instT3SpaceProdInstTopologicalSpaceProd {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T3Space α] [T3Space β] : T3Space (α × β)

Equations

• @instT3SpaceProdInstTopologicalSpaceProd = @instT3SpaceProdInstTopologicalSpaceProd.proof_1

instance instT3SpaceForAllTopologicalSpace {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), T3Space (π i)] : T3Space ((i : ι) → π i)

Equations

• @instT3SpaceForAllTopologicalSpace = @instT3SpaceForAllTopologicalSpace.proof_1

theorem disjoint_nested_nhds {α : Type u} [TopologicalSpace α] [T3Space α] {x : α} {y : α} (h : x ≠ y) : ∃ U₁, U₁ ∈ nhds x ∧ ∃ V₁, V₁ ∈ nhds x ∧ ∃ U₂, U₂ ∈ nhds y ∧ ∃ V₂, 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 {α : Type u} [TopologicalSpace α] [RegularSpace α] : T3Space (SeparationQuotient α)

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

Equations

• @instT3SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient = @instT3SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient.proof_1

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

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

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

theorem normal_separation {α : Type u} [TopologicalSpace α] [NormalSpace α] {s : Set α} {t : Set α} (H1 : IsClosed s) (H2 : IsClosed t) (H3 : Disjoint s t) : SeparatedNhds s t

theorem disjoint_nhdsSet_nhdsSet {α : Type u} [TopologicalSpace α] [NormalSpace α] {s : Set α} {t : Set α} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : Disjoint (nhdsSet s) (nhdsSet t)

theorem normal_exists_closure_subset {α : Type u} [TopologicalSpace α] [NormalSpace α] {s : Set α} {t : Set α} (hs : IsClosed s) (ht : IsOpen t) (hst : s ⊆ t) : ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t

theorem ClosedEmbedding.normalSpace {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [NormalSpace β] {f : α → β} (hf : ClosedEmbedding f) : NormalSpace α

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

instance NormalSpace.of_regularSpace_secondCountableTopology {α : Type u} [TopologicalSpace α] [RegularSpace α] [TopologicalSpace.SecondCountableTopology α] : NormalSpace α

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

Equations

• @NormalSpace.of_regularSpace_secondCountableTopology = @NormalSpace.of_regularSpace_secondCountableTopology.proof_1

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

A T₄ space is a normal T₁ space.

instance instT4Space {α : Type u} [TopologicalSpace α] [T1Space α] [NormalSpace α] : T4Space α

Equations

• (_ : T4Space α) = (_ : T4Space α)

instance T4Space.t3Space {α : Type u} [TopologicalSpace α] [T4Space α] : T3Space α

Equations

• @T4Space.t3Space = @T4Space.t3Space.proof_1

instance T4Space.of_compactSpace_t2Space {α : Type u} [TopologicalSpace α] [CompactSpace α] [T2Space α] : T4Space α

Equations

• @T4Space.of_compactSpace_t2Space = @T4Space.of_compactSpace_t2Space.proof_1

theorem ClosedEmbedding.t4Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T4Space β] {f : α → β} (hf : ClosedEmbedding f) : T4Space α

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

instance SeparationQuotient.instNormalSpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient {α : Type u} [TopologicalSpace α] [NormalSpace α] : NormalSpace (SeparationQuotient α)

The SeparationQuotient of a normal space is a normal space.

Equations

• @SeparationQuotient.instNormalSpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient = @SeparationQuotient.instNormalSpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient.proof_1

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

• t1 : ∀ (x : α), IsClosed {x}
• completely_normal : ∀ ⦃s t : Set α⦄, 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.

A topological space α is a completely normal Hausdorff space if each subspace s : Set α is a normal Hausdorff space. Equivalently, α 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.

theorem Embedding.t5Space {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [T5Space β] {e : α → β} (he : Embedding e) : T5Space α

instance instT5SpaceSubtypeInstTopologicalSpaceSubtype {α : Type u} [TopologicalSpace α] [T5Space α] {p : α → Prop} : T5Space { x // p x }

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

Equations

• @instT5SpaceSubtypeInstTopologicalSpaceSubtype = @instT5SpaceSubtypeInstTopologicalSpaceSubtype.proof_1

instance T5Space.toT4Space {α : Type u} [TopologicalSpace α] [T5Space α] : T4Space α

A T₅ space is a T₄ space.

Equations

• @T5Space.toT4Space = @T5Space.toT4Space.proof_1

instance instT5SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient {α : Type u} [TopologicalSpace α] [T5Space α] : T5Space (SeparationQuotient α)

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 α and SeparationQuotient α. We give an alternative proof of the completely_normal axiom that works without assuming that α is a T₁ space.

Equations

• @instT5SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient = @instT5SpaceSeparationQuotientInstTopologicalSpaceSeparationQuotient.proof_1

theorem connectedComponent_eq_iInter_clopen {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] (x : α) : connectedComponent x = ⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z

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

theorem totallySeparatedSpace_of_t1_of_basis_clopen {α : Type u} [TopologicalSpace α] [T1Space α] (h : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}) : TotallySeparatedSpace α

A T1 space with a clopen basis is totally separated.

theorem compact_t2_tot_disc_iff_tot_sep {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] : TotallyDisconnectedSpace α ↔ TotallySeparatedSpace α

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 {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] [TotallyDisconnectedSpace α] : TotallySeparatedSpace α

A totally disconnected compact Hausdorff space is totally separated.

Equations

• @instTotallySeparatedSpace = @instTotallySeparatedSpace.proof_1

theorem nhds_basis_clopen {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] [TotallyDisconnectedSpace α] (x : α) : Filter.HasBasis (nhds x) (fun s => x ∈ s ∧ IsClopen s) id

theorem isTopologicalBasis_clopen {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] [TotallyDisconnectedSpace α] : TopologicalSpace.IsTopologicalBasis {s | IsClopen s}

theorem compact_exists_clopen_in_open {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] [TotallyDisconnectedSpace α] {x : α} {U : Set α} (is_open : IsOpen U) (memU : x ∈ U) : ∃ V, 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_1} [TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] : TopologicalSpace.IsTopologicalBasis {s | 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_1} [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 {α : Type u} [TopologicalSpace α] [T2Space α] [CompactSpace α] : T2Space (ConnectedComponents α)

ConnectedComponents α is Hausdorff when α is Hausdorff and compact

Equations

• @ConnectedComponents.t2 = @ConnectedComponents.t2.proof_1