mathlib documentation

def separated_nhds {α : Type u} [topological_space α] :

set α → set α → Prop

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

Equations

separated_nhds = λ (s t : set α), ∃ (U V : set α), is_open U ∧ is_open V ∧ s ⊆ U ∧ t ⊆ V ∧ disjoint U V

theorem separated_nhds_iff_disjoint {α : Type u} [topological_space α] {s t : set α} :

separated_nhds s t ↔ disjoint (nhds_set s) (nhds_set t)

@[symm]

theorem separated_nhds.symm {α : Type u} [topological_space α] {s t : set α} :

separated_nhds s t → separated_nhds t s

theorem separated_nhds.comm {α : Type u} [topological_space α] (s t : set α) :

separated_nhds s t ↔ separated_nhds t s

theorem separated_nhds.preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} {s t : set β} (h : separated_nhds s t) (hf : continuous f) :

separated_nhds (f ⁻¹' s) (f ⁻¹' t)

@[protected]

theorem separated_nhds.disjoint {α : Type u} [topological_space α] {s t : set α} (h : separated_nhds s t) :

disjoint s t

theorem separated_nhds.disjoint_closure_left {α : Type u} [topological_space α] {s t : set α} (h : separated_nhds s t) :

disjoint (closure s) t

theorem separated_nhds.disjoint_closure_right {α : Type u} [topological_space α] {s t : set α} (h : separated_nhds s t) :

disjoint s (closure t)

theorem separated_nhds.empty_right {α : Type u} [topological_space α] (s : set α) :

separated_nhds s ∅

theorem separated_nhds.empty_left {α : Type u} [topological_space α] (s : set α) :

separated_nhds ∅ s

theorem separated_nhds.mono {α : Type u} [topological_space α] {s₁ s₂ t₁ t₂ : set α} (h : separated_nhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) :

separated_nhds s₁ t₁

theorem separated_nhds.union_left {α : Type u} [topological_space α] {s t u : set α} :

separated_nhds s u → separated_nhds t u → separated_nhds (s ∪ t) u

theorem separated_nhds.union_right {α : Type u} [topological_space α] {s t u : set α} (ht : separated_nhds s t) (hu : separated_nhds s u) :

separated_nhds s (t ∪ u)

@[class]

structure t0_space (α : Type u) [topological_space α] :

Prop

t0 : ∀ ⦃x y : α⦄, inseparable x y → x = y

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.

Instances of this typeclass

theorem t0_space_iff_inseparable (α : Type u) [topological_space α] :

t0_space α ↔ ∀ (x y : α), inseparable x y → x = y

theorem t0_space_iff_not_inseparable (α : Type u) [topological_space α] :

t0_space α ↔ ∀ (x y : α), x ≠ y → ¬inseparable x y

theorem inseparable.eq {α : Type u} [topological_space α] [t0_space α] {x y : α} (h : inseparable x y) :

x = y

theorem t0_space_iff_nhds_injective (α : Type u) [topological_space α] :

t0_space α ↔ function.injective nhds

theorem nhds_injective {α : Type u} [topological_space α] [t0_space α] :

function.injective nhds

theorem inseparable_iff_eq {α : Type u} [topological_space α] [t0_space α] {x y : α} :

inseparable x y ↔ x = y

@[simp]

theorem nhds_eq_nhds_iff {α : Type u} [topological_space α] [t0_space α] {a b : α} :

nhds a = nhds b ↔ a = b

@[simp]

theorem inseparable_eq_eq {α : Type u} [topological_space α] [t0_space α] :

inseparable = eq

theorem t0_space_iff_exists_is_open_xor_mem (α : Type u) [topological_space α] :

t0_space α ↔ ∀ (x y : α), x ≠ y → (∃ (U : set α), is_open U ∧ xor (x ∈ U) (y ∈ U))

theorem exists_is_open_xor_mem {α : Type u} [topological_space α] [t0_space α] {x y : α} (h : x ≠ y) :

∃ (U : set α), is_open U ∧ xor (x ∈ U) (y ∈ U)

def specialization_order (α : Type u_1) [topological_space α] [t0_space α] :

partial_order α

Specialization forms a partial order on a t0 topological space.

Equations

specialization_order α = {le := preorder.le (specialization_preorder α), lt := preorder.lt (specialization_preorder α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

@[protected, instance]

def separation_quotient.t0_space {α : Type u} [topological_space α] :

t0_space (separation_quotient α)

theorem minimal_nonempty_closed_subsingleton {α : Type u} [topological_space α] [t0_space α] {s : set α} (hs : is_closed s) (hmin : ∀ (t : set α), t ⊆ s → t.nonempty → is_closed t → t = s) :

s.subsingleton

theorem minimal_nonempty_closed_eq_singleton {α : Type u} [topological_space α] [t0_space α] {s : set α} (hs : is_closed s) (hne : s.nonempty) (hmin : ∀ (t : set α), t ⊆ s → t.nonempty → is_closed t → t = s) :

∃ (x : α), s = {x}

theorem is_closed.exists_closed_singleton {α : Type u_1} [topological_space α] [t0_space α] [compact_space α] {S : set α} (hS : is_closed S) (hne : S.nonempty) :

∃ (x : α), x ∈ S ∧ is_closed {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} [topological_space α] [t0_space α] {s : set α} (hs : is_open s) (hmin : ∀ (t : set α), t ⊆ s → t.nonempty → is_open t → t = s) :

s.subsingleton

theorem minimal_nonempty_open_eq_singleton {α : Type u} [topological_space α] [t0_space α] {s : set α} (hs : is_open s) (hne : s.nonempty) (hmin : ∀ (t : set α), t ⊆ s → t.nonempty → is_open t → t = s) :

∃ (x : α), s = {x}

theorem exists_open_singleton_of_open_finite {α : Type u} [topological_space α] [t0_space α] {s : set α} (hfin : s.finite) (hne : s.nonempty) (ho : is_open s) :

∃ (x : α) (H : x ∈ s), is_open {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_fintype {α : Type u} [topological_space α] [t0_space α] [finite α] [nonempty α] :

∃ (x : α), is_open {x}

theorem t0_space_of_injective_of_continuous {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : function.injective f) (hf' : continuous f) [t0_space β] :

@[protected]

theorem embedding.t0_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t0_space β] {f : α → β} (hf : embedding f) :

@[protected, instance]

def subtype.t0_space {α : Type u} [topological_space α] [t0_space α] {p : α → Prop} :

t0_space (subtype p)

theorem t0_space_iff_or_not_mem_closure (α : Type u) [topological_space α] :

t0_space α ↔ ∀ (a b : α), a ≠ b → a ∉ closure {b} ∨ b ∉ closure {a}

@[protected, instance]

def prod.t0_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t0_space α] [t0_space β] :

t0_space (α × β)

@[protected, instance]

def pi.t0_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), t0_space (π i)] :

t0_space (Π (i : ι), π i)

theorem t0_space.of_cover {α : Type u} [topological_space α] (h : ∀ (x y : α), inseparable x y → (∃ (s : set α), x ∈ s ∧ y ∈ s ∧ t0_space ↥s)) :

theorem t0_space.of_open_cover {α : Type u} [topological_space α] (h : ∀ (x : α), ∃ (s : set α), x ∈ s ∧ is_open s ∧ t0_space ↥s) :

@[class]

structure t1_space (α : Type u) [topological_space α] :

Prop

t1 : ∀ (x : α), is_closed {x}

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

Instances of this typeclass

theorem is_closed_singleton {α : Type u} [topological_space α] [t1_space α] {x : α} :

is_closed {x}

theorem is_open_compl_singleton {α : Type u} [topological_space α] [t1_space α] {x : α} :

is_open {x}ᶜ

theorem is_open_ne {α : Type u} [topological_space α] [t1_space α] {x : α} :

is_open {y : α | y ≠ x}

theorem continuous.is_open_support {α : Type u} {β : Type v} [topological_space α] [t1_space α] [has_zero α] [topological_space β] {f : β → α} (hf : continuous f) :

is_open (function.support f)

theorem continuous.is_open_mul_support {α : Type u} {β : Type v} [topological_space α] [t1_space α] [has_one α] [topological_space β] {f : β → α} (hf : continuous f) :

is_open (function.mul_support f)

theorem ne.nhds_within_compl_singleton {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x ≠ y) :

nhds_within x {y}ᶜ = nhds x

theorem ne.nhds_within_diff_singleton {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x ≠ y) (s : set α) :

nhds_within x (s \ {y}) = nhds_within x s

theorem is_open_set_of_eventually_nhds_within {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :

is_open {x : α | ∀ᶠ (y : α) in nhds_within x {x}ᶜ, p y}

@[protected]

theorem set.finite.is_closed {α : Type u} [topological_space α] [t1_space α] {s : set α} (hs : s.finite) :

is_closed s

theorem topological_space.is_topological_basis.exists_mem_of_ne {α : Type u} [topological_space α] [t1_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {x y : α} (h : x ≠ y) :

∃ (a : set α) (H : a ∈ b), x ∈ a ∧ y ∉ a

theorem filter.coclosed_compact_le_cofinite {α : Type u} [topological_space α] [t1_space α] :

filter.coclosed_compact α ≤ filter.cofinite

def bornology.relatively_compact (α : Type u) [topological_space α] [t1_space α] :

bornology α

In a t1_space, relatively compact sets form a bornology. Its cobounded filter is filter.coclosed_compact. See also bornology.in_compact the bornology of sets contained in a compact set.

Equations

bornology.relatively_compact α = {cobounded := filter.coclosed_compact α _inst_1, le_cofinite := _}

theorem bornology.relatively_compact.is_bounded_iff {α : Type u} [topological_space α] [t1_space α] {s : set α} :

bornology.is_bounded s ↔ is_compact (closure s)

@[protected]

theorem finset.is_closed {α : Type u} [topological_space α] [t1_space α] (s : finset α) :

is_closed ↑s

theorem t1_space_tfae (α : Type u) [topological_space α] :

[t1_space α, ∀ (x : α), is_closed {x}, ∀ (x : α), is_open {x}ᶜ, continuous ⇑cofinite_topology.of, ∀ ⦃x y : α⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : α⦄, x ≠ y → (∃ (s : set α) (H : s ∈ nhds x), y ∉ s), ∀ ⦃x y : α⦄, x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U), ∀ ⦃x y : α⦄, x ≠ y → disjoint (nhds x) (has_pure.pure y), ∀ ⦃x y : α⦄, x ≠ y → disjoint (has_pure.pure x) (nhds y), ∀ ⦃x y : α⦄, x ⤳ y → x = y].tfae

theorem t1_space_iff_continuous_cofinite_of {α : Type u_1} [topological_space α] :

t1_space α ↔ continuous ⇑cofinite_topology.of

continuous ⇑cofinite_topology.of

theorem cofinite_topology.continuous_of {α : Type u} [topological_space α] [t1_space α] :

theorem t1_space_iff_exists_open {α : Type u} [topological_space α] :

t1_space α ↔ ∀ (x y : α), x ≠ y → (∃ (U : set α) (hU : is_open U), x ∈ U ∧ y ∉ U)

theorem t1_space_iff_disjoint_pure_nhds {α : Type u} [topological_space α] :

t1_space α ↔ ∀ ⦃x y : α⦄, x ≠ y → disjoint (has_pure.pure x) (nhds y)

theorem t1_space_iff_disjoint_nhds_pure {α : Type u} [topological_space α] :

t1_space α ↔ ∀ ⦃x y : α⦄, x ≠ y → disjoint (nhds x) (has_pure.pure y)

theorem t1_space_iff_specializes_imp_eq {α : Type u} [topological_space α] :

t1_space α ↔ ∀ ⦃x y : α⦄, x ⤳ y → x = y

theorem disjoint_pure_nhds {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x ≠ y) :

disjoint (has_pure.pure x) (nhds y)

theorem disjoint_nhds_pure {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x ≠ y) :

disjoint (nhds x) (has_pure.pure y)

theorem specializes.eq {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x ⤳ y) :

x = y

theorem specializes_iff_eq {α : Type u} [topological_space α] [t1_space α] {x y : α} :

x ⤳ y ↔ x = y

@[simp]

theorem specializes_eq_eq {α : Type u} [topological_space α] [t1_space α] :

specializes = eq

@[simp]

theorem pure_le_nhds_iff {α : Type u} [topological_space α] [t1_space α] {a b : α} :

has_pure.pure a ≤ nhds b ↔ a = b

@[simp]

theorem nhds_le_nhds_iff {α : Type u} [topological_space α] [t1_space α] {a b : α} :

nhds a ≤ nhds b ↔ a = b

@[protected, instance]

def cofinite_topology.t1_space {α : Type u_1} :

t1_space (cofinite_topology α)

theorem t1_space_antitone {α : Type u_1} :

antitone (t1_space α)

theorem continuous_within_at_update_of_ne {α : Type u} {β : Type v} [topological_space α] [t1_space α] [decidable_eq α] [topological_space β] {f : α → β} {s : set α} {x y : α} {z : β} (hne : y ≠ x) :

continuous_within_at (function.update f x z) s y ↔ continuous_within_at f s y

theorem continuous_at_update_of_ne {α : Type u} {β : Type v} [topological_space α] [t1_space α] [decidable_eq α] [topological_space β] {f : α → β} {x y : α} {z : β} (hne : y ≠ x) :

continuous_at (function.update f x z) y ↔ continuous_at f y

theorem continuous_on_update_iff {α : Type u} {β : Type v} [topological_space α] [t1_space α] [decidable_eq α] [topological_space β] {f : α → β} {s : set α} {x : α} {y : β} :

continuous_on (function.update f x y) s ↔ continuous_on f (s \ {x}) ∧ (x ∈ s → filter.tendsto f (nhds_within x (s \ {x})) (nhds y))

theorem t1_space_of_injective_of_continuous {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : function.injective f) (hf' : continuous f) [t1_space β] :

t1_space α

@[protected]

theorem embedding.t1_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space β] {f : α → β} (hf : embedding f) :

t1_space α

@[protected, instance]

def subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :

t1_space (subtype p)

@[protected, instance]

def prod.t1_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space α] [t1_space β] :

t1_space (α × β)

@[protected, instance]

def pi.t1_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), t1_space (π i)] :

t1_space (Π (i : ι), π i)

@[protected, instance]

def t1_space.t0_space {α : Type u} [topological_space α] [t1_space α] :

@[simp]

theorem compl_singleton_mem_nhds_iff {α : Type u} [topological_space α] [t1_space α] {x y : α} :

{x}ᶜ ∈ nhds y ↔ y ≠ x

theorem compl_singleton_mem_nhds {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : y ≠ x) :

{x}ᶜ ∈ nhds y

@[simp]

theorem closure_singleton {α : Type u} [topological_space α] [t1_space α] {a : α} :

closure {a} = {a}

theorem set.subsingleton.closure {α : Type u} [topological_space α] [t1_space α] {s : set α} (hs : s.subsingleton) :

(closure s).subsingleton

@[simp]

theorem subsingleton_closure {α : Type u} [topological_space α] [t1_space α] {s : set α} :

(closure s).subsingleton ↔ s.subsingleton

theorem is_closed_map_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t1_space β] {y : β} :

is_closed_map (function.const α y)

theorem nhds_within_insert_of_ne {α : Type u} [topological_space α] [t1_space α] {x y : α} {s : set α} (hxy : x ≠ y) :

nhds_within x (has_insert.insert y s) = nhds_within x s

theorem insert_mem_nhds_within_of_subset_insert {α : Type u} [topological_space α] [t1_space α] {x y : α} {s t : set α} (hu : t ⊆ has_insert.insert y s) :

has_insert.insert x s ∈ nhds_within x t

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

theorem bInter_basis_nhds {α : Type u} [topological_space α] [t1_space α] {ι : Sort u_1} {p : ι → Prop} {s : ι → set α} {x : α} (h : (nhds x).has_basis p s) :

(⋂ (i : ι) (h : p i), s i) = {x}

@[simp]

theorem compl_singleton_mem_nhds_set_iff {α : Type u} [topological_space α] [t1_space α] {x : α} {s : set α} :

{x}ᶜ ∈ nhds_set s ↔ x ∉ s

@[simp]

theorem nhds_set_le_iff {α : Type u} [topological_space α] [t1_space α] {s t : set α} :

nhds_set s ≤ nhds_set t ↔ s ⊆ t

@[simp]

theorem nhds_set_inj_iff {α : Type u} [topological_space α] [t1_space α] {s t : set α} :

nhds_set s = nhds_set t ↔ s = t

function.injective nhds_set

theorem injective_nhds_set {α : Type u} [topological_space α] [t1_space α] :

theorem strict_mono_nhds_set {α : Type u} [topological_space α] [t1_space α] :

strict_mono nhds_set

@[simp]

theorem nhds_le_nhds_set_iff {α : Type u} [topological_space α] [t1_space α] {s : set α} {x : α} :

nhds x ≤ nhds_set s ↔ x ∈ s

theorem dense.diff_singleton {α : Type u} [topological_space α] [t1_space α] {s : set α} (hs : dense s) (x : α) [(nhds_within x {x}ᶜ).ne_bot] :

dense (s \ {x})

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

theorem dense.diff_finset {α : Type u} [topological_space α] [t1_space α] [∀ (x : α), (nhds_within x {x}ᶜ).ne_bot] {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} [topological_space α] [t1_space α] [∀ (x : α), (nhds_within x {x}ᶜ).ne_bot] {s : set α} (hs : dense s) {t : set α} (ht : t.finite) :

dense (s \ t)

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

theorem eq_of_tendsto_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space β] {f : α → β} {a : α} {b : β} (h : filter.tendsto f (nhds a) (nhds b)) :

f a = b

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

theorem filter.tendsto.eventually_ne {β : Type v} [topological_space β] [t1_space β] {α : 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 continuous_at.eventually_ne {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space β] {g : α → β} {a : α} {b : β} (hg1 : continuous_at g a) (hg2 : g a ≠ b) :

∀ᶠ (z : α) in nhds a, g z ≠ b

theorem continuous_at_of_tendsto_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space β] {f : α → β} {a : α} {b : β} (h : filter.tendsto f (nhds a) (nhds b)) :

continuous_at f a

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

theorem tendsto_const_nhds_iff {α : Type u} [topological_space α] [t1_space α] {l : filter α} [l.ne_bot] {c d : α} :

filter.tendsto (λ (x : α), c) l (nhds d) ↔ c = d

theorem infinite_of_mem_nhds {α : Type u_1} [topological_space α] [t1_space α] (x : α) [hx : (nhds_within x {x}ᶜ).ne_bot] {s : set α} (hs : s ∈ nhds x) :

s.infinite

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

theorem discrete_of_t1_of_finite {X : Type u_1} [topological_space X] [t1_space X] [finite X] :

discrete_topology X

theorem preconnected_space.trivial_of_discrete {α : Type u} [topological_space α] [preconnected_space α] [discrete_topology α] :

subsingleton α

theorem is_preconnected.infinite_of_nontrivial {α : Type u} [topological_space α] [t1_space α] {s : set α} (h : is_preconnected s) (hs : s.nontrivial) :

s.infinite

theorem connected_space.infinite {α : Type u} [topological_space α] [connected_space α] [nontrivial α] [t1_space α] :

infinite α

theorem singleton_mem_nhds_within_of_mem_discrete {α : Type u} [topological_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :

{x} ∈ nhds_within x s

theorem nhds_within_of_mem_discrete {α : Type u} [topological_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :

nhds_within x s = has_pure.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.has_basis.exists_inter_eq_singleton_of_mem_discrete {α : Type u} [topological_space α] {ι : Type u_1} {p : ι → Prop} {t : ι → set α} {s : set α} [discrete_topology ↥s] {x : α} (hb : (nhds x).has_basis p t) (hx : x ∈ s) :

∃ (i : ι) (hi : p i), t i ∩ s = {x}

theorem nhds_inter_eq_singleton_of_mem_discrete {α : Type u} [topological_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :

∃ (U : set α) (H : 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_nhds_within_of_mem_discrete {α : Type u} [topological_space α] {s : set α} [discrete_topology ↥s] {x : α} (hx : x ∈ s) :

∃ (U : set α) (H : U ∈ nhds_within x {x}ᶜ), disjoint U s

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

U is a punctured neighborhood of x (ie. U ∪ {x} is a neighbourhood of x),
U is disjoint from s.

subtype.topological_space = topological_space.induced (set.inclusion ts) subtype.topological_space

theorem topological_space.subset_trans {X : Type u_1} [tX : topological_space X] {s t : set X} (ts : t ⊆ s) :

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.

theorem induced_bot {X : Type u_1} {Y : Type u_2} {f : X → Y} (hf : function.injective f) :

topological_space.induced f ⊥ = ⊥

The topology pulled-back under an inclusion f : X → Y from the discrete topology (⊥) is the discrete topology. This version does not assume the choice of a topology on either the source X nor the target Y of the inclusion f.

theorem discrete_topology_induced {X : Type u_1} {Y : Type u_2} [tY : topological_space Y] [discrete_topology Y] {f : X → Y} (hf : function.injective f) :

discrete_topology X

The topology induced under an inclusion f : X → Y from the discrete topological space Y is the discrete topology on X.

theorem embedding.discrete_topology {X : Type u_1} {Y : Type u_2} [topological_space X] [tY : topological_space Y] [discrete_topology Y] {f : X → Y} (hf : embedding f) :

discrete_topology X

theorem discrete_topology.of_subset {X : Type u_1} [topological_space X] {s t : set X} (ds : discrete_topology ↥s) (ts : t ⊆ s) :

discrete_topology ↥t

Let s, t ⊆ X be two subsets of a topological space X. If t ⊆ s and the topology induced by Xon s is discrete, then also the topology induces on t is discrete.

@[class]

structure t2_space (α : Type u) [topological_space α] :

Prop

t2 : ∀ (x y : α), x ≠ y → (∃ (u v : set α), is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ disjoint u v)

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

Instances of this typeclass

theorem t2_space_iff (α : Type u) [topological_space α] :

t2_space α ↔ ∀ (x y : α), x ≠ y → (∃ (u v : set α), is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ disjoint u v)

theorem t2_separation {α : Type u} [topological_space α] [t2_space α] {x y : α} (h : x ≠ y) :

∃ (u v : set α), is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ disjoint u v

Two different points can be separated by open sets.

theorem t2_space_iff_disjoint_nhds {α : Type u} [topological_space α] :

t2_space α ↔ ∀ (x y : α), x ≠ y → disjoint (nhds x) (nhds y)

@[simp]

theorem disjoint_nhds_nhds {α : Type u} [topological_space α] [t2_space α] {x y : α} :

disjoint (nhds x) (nhds y) ↔ x ≠ y

theorem pairwise_disjoint_nhds {α : Type u} [topological_space α] [t2_space α] :

pairwise (disjoint on nhds)

@[protected]

theorem set.pairwise_disjoint_nhds {α : Type u} [topological_space α] [t2_space α] (s : set α) :

s.pairwise_disjoint nhds

theorem set.finite.t2_separation {α : Type u} [topological_space α] [t2_space α] {s : set α} (hs : s.finite) :

∃ (U : α → set α), (∀ (x : α), x ∈ U x ∧ is_open (U x)) ∧ s.pairwise_disjoint U

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

theorem is_open_set_of_disjoint_nhds_nhds {α : Type u} [topological_space α] :

is_open {p : α × α | disjoint (nhds p.fst) (nhds p.snd)}

@[protected, instance]

def t2_space.t1_space {α : Type u} [topological_space α] [t2_space α] :

t1_space α

theorem t2_iff_nhds {α : Type u} [topological_space α] :

t2_space α ↔ ∀ {x y : α}, (nhds x ⊓ nhds y).ne_bot → x = y

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

theorem eq_of_nhds_ne_bot {α : Type u} [topological_space α] [t2_space α] {x y : α} (h : (nhds x ⊓ nhds y).ne_bot) :

x = y

theorem t2_space_iff_nhds {α : Type u} [topological_space α] :

t2_space α ↔ ∀ {x y : α}, x ≠ y → (∃ (U : set α) (H : U ∈ nhds x) (V : set α) (H : V ∈ nhds y), disjoint U V)

theorem t2_separation_nhds {α : Type u} [topological_space α] [t2_space α] {x y : α} (h : x ≠ y) :

∃ (u v : set α), u ∈ nhds x ∧ v ∈ nhds y ∧ disjoint u v

theorem t2_separation_compact_nhds {α : Type u} [topological_space α] [locally_compact_space α] [t2_space α] {x y : α} (h : x ≠ y) :

∃ (u v : set α), u ∈ nhds x ∧ v ∈ nhds y ∧ is_compact u ∧ is_compact v ∧ disjoint u v

theorem t2_iff_ultrafilter {α : Type u} [topological_space α] :

t2_space α ↔ ∀ {x y : α} (f : ultrafilter α), ↑f ≤ nhds x → ↑f ≤ nhds y → x = y

theorem t2_iff_is_closed_diagonal {α : Type u} [topological_space α] :

t2_space α ↔ is_closed (set.diagonal α)

theorem is_closed_diagonal {α : Type u} [topological_space α] [t2_space α] :

is_closed (set.diagonal α)

theorem finset_disjoint_finset_opens_of_t2 {α : Type u} [topological_space α] [t2_space α] (s t : finset α) :

disjoint s t → separated_nhds ↑s ↑t

theorem point_disjoint_finset_opens_of_t2 {α : Type u} [topological_space α] [t2_space α] {x : α} {s : finset α} (h : x ∉ s) :

separated_nhds {x} ↑s

theorem tendsto_nhds_unique {α : Type u} {β : Type v} [topological_space α] [t2_space α] {f : β → α} {l : filter β} {a b : α} [l.ne_bot] (ha : filter.tendsto f l (nhds a)) (hb : filter.tendsto f l (nhds b)) :

a = b

theorem tendsto_nhds_unique' {α : Type u} {β : Type v} [topological_space α] [t2_space α] {f : β → α} {l : filter β} {a b : α} (hl : l.ne_bot) (ha : filter.tendsto f l (nhds a)) (hb : filter.tendsto f l (nhds b)) :

a = b

theorem tendsto_nhds_unique_of_eventually_eq {α : Type u} {β : Type v} [topological_space α] [t2_space α] {f g : β → α} {l : filter β} {a b : α} [l.ne_bot] (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} [topological_space α] [t2_space α] {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]

structure t2_5_space (α : Type u) [topological_space α] :

Prop

t2_5 : ∀ ⦃x y : α⦄, x ≠ y → disjoint ((nhds x).lift' closure) ((nhds y).lift' closure)

A T₂.₅ space, also known as a Urysohn space, is a topological space where for every pair x ≠ y, there are two open sets, with the intersection of closures empty, one containing x and the other y .

Instances of this typeclass

t3_space.t2_5_space

@[simp]

theorem disjoint_lift'_closure_nhds {α : Type u} [topological_space α] [t2_5_space α] {x y : α} :

disjoint ((nhds x).lift' closure) ((nhds y).lift' closure) ↔ x ≠ y

@[protected, instance]

def t2_5_space.t2_space {α : Type u} [topological_space α] [t2_5_space α] :

t2_space α

theorem exists_nhds_disjoint_closure {α : Type u} [topological_space α] [t2_5_space α] {x y : α} (h : x ≠ y) :

∃ (s : set α) (H : s ∈ nhds x) (t : set α) (H : t ∈ nhds y), disjoint (closure s) (closure t)

theorem exists_open_nhds_disjoint_closure {α : Type u} [topological_space α] [t2_5_space α] {x y : α} (h : x ≠ y) :

∃ (u : set α), x ∈ u ∧ is_open u ∧ ∃ (v : set α), y ∈ v ∧ is_open v ∧ disjoint (closure u) (closure v)

Properties of `Lim` and `lim` #

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

theorem Lim_eq {α : Type u} [topological_space α] [t2_space α] {f : filter α} {a : α} [f.ne_bot] (h : f ≤ nhds a) :

Lim f = a

theorem Lim_eq_iff {α : Type u} [topological_space α] [t2_space α] {f : filter α} [f.ne_bot] (h : ∃ (a : α), f ≤ nhds a) {a : α} :

Lim f = a ↔ f ≤ nhds a

theorem ultrafilter.Lim_eq_iff_le_nhds {α : Type u} [topological_space α] [t2_space α] [compact_space α] {x : α} {F : ultrafilter α} :

F.Lim = x ↔ ↑F ≤ nhds x

theorem is_open_iff_ultrafilter' {α : Type u} [topological_space α] [t2_space α] [compact_space α] (U : set α) :

is_open U ↔ ∀ (F : ultrafilter α), F.Lim ∈ U → U ∈ F.to_filter

theorem filter.tendsto.lim_eq {α : Type u} {β : Type v} [topological_space α] [t2_space α] {a : α} {f : filter β} [f.ne_bot] {g : β → α} (h : filter.tendsto g f (nhds a)) :

lim f g = a

theorem filter.lim_eq_iff {α : Type u} {β : Type v} [topological_space α] [t2_space α] {f : filter β} [f.ne_bot] {g : β → α} (h : ∃ (a : α), filter.tendsto g f (nhds a)) {a : α} :

lim f g = a ↔ filter.tendsto g f (nhds a)

theorem continuous.lim_eq {α : Type u} {β : Type v} [topological_space α] [t2_space α] [topological_space β] {f : β → α} (h : continuous f) (a : β) :

lim (nhds a) f = f a

@[simp]

theorem Lim_nhds {α : Type u} [topological_space α] [t2_space α] (a : α) :

Lim (nhds a) = a

@[simp]

theorem lim_nhds_id {α : Type u} [topological_space α] [t2_space α] (a : α) :

lim (nhds a) id = a

@[simp]

theorem Lim_nhds_within {α : Type u} [topological_space α] [t2_space α] {a : α} {s : set α} (h : a ∈ closure s) :

Lim (nhds_within a s) = a

@[simp]

theorem lim_nhds_within_id {α : Type u} [topological_space α] [t2_space α] {a : α} {s : set α} (h : a ∈ closure s) :

lim (nhds_within a s) id = a

`t2_space` 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_open_embedding 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.

@[protected, instance]

def discrete_topology.to_t2_space {α : Type u_1} [topological_space α] [discrete_topology α] :

t2_space α

theorem separated_by_continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t2_space β] {f : α → β} (hf : continuous f) {x y : α} (h : f x ≠ f y) :

∃ (u v : set α), is_open u ∧ is_open v ∧ x ∈ u ∧ y ∈ v ∧ disjoint u v

theorem separated_by_open_embedding {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t2_space α] {f : α → β} (hf : open_embedding f) {x y : α} (h : x ≠ y) :

∃ (u v : set β), is_open u ∧ is_open v ∧ f x ∈ u ∧ f y ∈ v ∧ disjoint u v

@[protected, instance]

def subtype.t2_space {α : Type u_1} {p : α → Prop} [t : topological_space α] [t2_space α] :

t2_space (subtype p)

@[protected, instance]

def prod.t2_space {α : Type u_1} {β : Type u_2} [t₁ : topological_space α] [t2_space α] [t₂ : topological_space β] [t2_space β] :

t2_space (α × β)

theorem embedding.t2_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space β] {f : α → β} (hf : embedding f) :

t2_space α

@[protected, instance]

def sum.t2_space {α : Type u_1} {β : Type u_2} [t₁ : topological_space α] [t2_space α] [t₂ : topological_space β] [t2_space β] :

t2_space (α ⊕ β)

@[protected, instance]

def Pi.t2_space {α : Type u_1} {β : α → Type v} [t₂ : Π (a : α), topological_space (β a)] [∀ (a : α), t2_space (β a)] :

t2_space (Π (a : α), β a)

@[protected, instance]

def sigma.t2_space {ι : Type u_1} {α : ι → Type u_2} [Π (i : ι), topological_space (α i)] [∀ (a : ι), t2_space (α a)] :

t2_space (Σ (i : ι), α i)

theorem is_closed_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {f g : β → α} (hf : continuous f) (hg : continuous g) :

is_closed {x : β | f x = g x}

theorem is_open_ne_fun {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {f g : β → α} (hf : continuous f) (hg : continuous g) :

is_open {x : β | f x ≠ g x}

theorem set.eq_on.closure {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {s : set β} {f g : β → α} (h : set.eq_on f g s) (hf : continuous f) (hg : continuous g) :

set.eq_on f g (closure s)

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

theorem continuous.ext_on {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {s : set β} (hs : dense s) {f g : β → α} (hf : continuous f) (hg : continuous g) (h : set.eq_on f g s) :

f = g

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

theorem eq_on_closure₂' {α : Type u} {β : Type v} [topological_space α] {γ : Type u_1} [topological_space β] [topological_space γ] [t2_space α] {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 (λ (x : β), f x y)) (hg₁ : ∀ (x : β), continuous (g x)) (hg₂ : ∀ (y : γ), continuous (λ (x : β), g x y)) (x : β) (H : x ∈ closure s) (y : γ) (H_1 : y ∈ closure t) :

f x y = g x y

theorem eq_on_closure₂ {α : Type u} {β : Type v} [topological_space α] {γ : Type u_1} [topological_space β] [topological_space γ] [t2_space α] {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 : β) (H : x ∈ closure s) (y : γ) (H_1 : y ∈ closure t) :

f x y = g x y

theorem set.eq_on.of_subset_closure {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {s t : set β} {f g : β → α} (h : set.eq_on f g s) (hf : continuous_on f t) (hg : continuous_on g t) (hst : s ⊆ t) (hts : t ⊆ closure s) :

set.eq_on 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.eq_on.closure.

theorem function.left_inverse.closed_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {f : α → β} {g : β → α} (h : function.left_inverse f g) (hf : continuous f) (hg : continuous g) :

is_closed (set.range g)

theorem function.left_inverse.closed_embedding {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space α] {f : α → β} {g : β → α} (h : function.left_inverse f g) (hf : continuous f) (hg : continuous g) :

closed_embedding g

theorem is_compact_is_compact_separated {α : Type u} [topological_space α] [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : disjoint s t) :

separated_nhds s t

theorem is_compact.is_closed {α : Type u} [topological_space α] [t2_space α] {s : set α} (hs : is_compact s) :

is_closed s

In a t2_space, every compact set is closed.

@[simp]

theorem filter.coclosed_compact_eq_cocompact {α : Type u} [topological_space α] [t2_space α] :

filter.coclosed_compact α = filter.cocompact α

@[simp]

theorem bornology.relatively_compact_eq_in_compact {α : Type u} [topological_space α] [t2_space α] :

bornology.relatively_compact α = bornology.in_compact α

theorem exists_subset_nhds_of_is_compact {α : Type u} [topological_space α] [t2_space α] {ι : Type u_1} [nonempty ι] {V : ι → set α} (hV : directed superset V) (hV_cpct : ∀ (i : ι), is_compact (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_nhd_of_compact' where we don't need to assume each V i closed because it follows from compactness since α is assumed to be Hausdorff.

theorem compact_exhaustion.is_closed {α : Type u} [topological_space α] [t2_space α] (K : compact_exhaustion α) (n : ℕ) :

is_closed (⇑K n)

theorem is_compact.inter {α : Type u} [topological_space α] [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :

is_compact (s ∩ t)

theorem is_compact_closure_of_subset_compact {α : Type u} [topological_space α] [t2_space α] {s t : set α} (ht : is_compact t) (h : s ⊆ t) :

is_compact (closure s)

@[simp]

theorem exists_compact_superset_iff {α : Type u} [topological_space α] [t2_space α] {s : set α} :

(∃ (K : set α), is_compact K ∧ s ⊆ K) ↔ is_compact (closure s)

theorem image_closure_of_is_compact {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t2_space β] {s : set α} (hs : is_compact (closure s)) {f : α → β} (hf : continuous_on f (closure s)) :

f '' closure s = closure (f '' s)

theorem is_compact.binary_compact_cover {α : Type u} [topological_space α] [t2_space α] {K U V : set α} (hK : is_compact K) (hU : is_open U) (hV : is_open V) (h2K : K ⊆ U ∪ V) :

∃ (K₁ K₂ : set α), is_compact K₁ ∧ is_compact 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.is_closed_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [t2_space β] {f : α → β} (h : continuous f) :

is_closed_map f

theorem continuous.closed_embedding {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [t2_space β] {f : α → β} (h : continuous f) (hf : function.injective f) :

closed_embedding f

theorem is_compact.finite_compact_cover {α : Type u} [topological_space α] [t2_space α] {s : set α} (hs : is_compact s) {ι : Type u_1} (t : finset ι) (U : ι → set α) (hU : ∀ (i : ι), i ∈ t → is_open (U i)) (hsC : s ⊆ ⋃ (i : ι) (H : i ∈ t), U i) :

∃ (K : ι → set α), (∀ (i : ι), is_compact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ (i : ι) (H : i ∈ t), K i

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

theorem locally_compact_of_compact_nhds {α : Type u} [topological_space α] [t2_space α] (h : ∀ (x : α), ∃ (s : set α), s ∈ nhds x ∧ is_compact s) :

locally_compact_space α

@[protected, instance]

def locally_compact_of_compact {α : Type u} [topological_space α] [t2_space α] [compact_space α] :

locally_compact_space α

theorem exists_open_with_compact_closure {α : Type u} [topological_space α] [locally_compact_space α] [t2_space α] (x : α) :

∃ (U : set α), is_open U ∧ x ∈ U ∧ is_compact (closure U)

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

theorem exists_open_superset_and_is_compact_closure {α : Type u} [topological_space α] [locally_compact_space α] [t2_space α] {K : set α} (hK : is_compact K) :

∃ (V : set α), is_open V ∧ K ⊆ V ∧ is_compact (closure V)

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

theorem exists_open_between_and_is_compact_closure {α : Type u} [topological_space α] [locally_compact_space α] [t2_space α] {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K ⊆ U) :

∃ (V : set α), is_open V ∧ K ⊆ V ∧ closure V ⊆ U ∧ is_compact (closure V)

In a locally compact T₂ space, given a compact set K inside an open set U, we can find a open set V between these sets with compact closure: K ⊆ V and the closure of V is inside U.

theorem is_preirreducible_iff_subsingleton {α : Type u} [topological_space α] [t2_space α] {S : set α} :

is_preirreducible S ↔ S.subsingleton

@[protected]

theorem is_preirreducible.subsingleton {α : Type u} [topological_space α] [t2_space α] {S : set α} :

is_preirreducible S → S.subsingleton

Alias of the forward direction of is_preirreducible_iff_subsingleton.

theorem is_irreducible_iff_singleton {α : Type u} [topological_space α] [t2_space α] {S : set α} :

is_irreducible S ↔ ∃ (x : α), S = {x}

theorem not_preirreducible_nontrivial_t2 (α : Type u_1) [topological_space α] [preirreducible_space α] [nontrivial α] [t2_space α] :

false

There does not exist a nontrivial preirreducible T₂ space.

theorem regular_space_iff (X : Type u) [topological_space X] :

regular_space X ↔ ∀ {s : set X} {a : X}, is_closed s → a ∉ s → disjoint (nhds_set s) (nhds a)

@[class]

structure regular_space (X : Type u) [topological_space X] :

Prop

regular : ∀ {s : set X} {a : X}, is_closed s → a ∉ s → disjoint (nhds_set s) (nhds a)

A topological space is called a regular space if for any closed set s and a ∉ s, there exist disjoint open sets U ⊇ s and V ∋ a. We formulate this condition in terms of disjointness of filters 𝓝ˢ s and 𝓝 a.

Instances of this typeclass

theorem regular_space_tfae (X : Type u) [topological_space X] :

[regular_space X, ∀ (s : set X) (a : X), a ∉ closure s → disjoint (nhds_set s) (nhds a), ∀ (a : X) (s : set X), disjoint (nhds_set s) (nhds a) ↔ a ∉ closure s, ∀ (a : X) (s : set X), s ∈ nhds a → (∃ (t : set X) (H : t ∈ nhds a), is_closed t ∧ t ⊆ s), ∀ (a : X), (nhds a).lift' closure ≤ nhds a, ∀ (a : X), (nhds a).lift' closure = nhds a].tfae

theorem regular_space.of_lift'_closure {α : Type u} [topological_space α] (h : ∀ (a : α), (nhds a).lift' closure = nhds a) :

regular_space α

theorem regular_space.of_basis {α : Type u} [topological_space α] {ι : α → Sort u_1} {p : Π (a : α), ι a → Prop} {s : Π (a : α), ι a → set α} (h₁ : ∀ (a : α), (nhds a).has_basis (p a) (s a)) (h₂ : ∀ (a : α) (i : ι a), p a i → is_closed (s a i)) :

regular_space α

theorem regular_space.of_exists_mem_nhds_is_closed_subset {α : Type u} [topological_space α] (h : ∀ (a : α) (s : set α), s ∈ nhds a → (∃ (t : set α) (H : t ∈ nhds a), is_closed t ∧ t ⊆ s)) :

regular_space α

theorem disjoint_nhds_set_nhds {α : Type u} [topological_space α] [regular_space α] {a : α} {s : set α} :

disjoint (nhds_set s) (nhds a) ↔ a ∉ closure s

theorem disjoint_nhds_nhds_set {α : Type u} [topological_space α] [regular_space α] {a : α} {s : set α} :

disjoint (nhds a) (nhds_set s) ↔ a ∉ closure s

theorem exists_mem_nhds_is_closed_subset {α : Type u} [topological_space α] [regular_space α] {a : α} {s : set α} (h : s ∈ nhds a) :

∃ (t : set α) (H : t ∈ nhds a), is_closed t ∧ t ⊆ s

theorem closed_nhds_basis {α : Type u} [topological_space α] [regular_space α] (a : α) :

(nhds a).has_basis (λ (s : set α), s ∈ nhds a ∧ is_closed s) id

theorem lift'_nhds_closure {α : Type u} [topological_space α] [regular_space α] (a : α) :

(nhds a).lift' closure = nhds a

theorem filter.has_basis.nhds_closure {α : Type u} [topological_space α] [regular_space α] {ι : Sort u_1} {a : α} {p : ι → Prop} {s : ι → set α} (h : (nhds a).has_basis p s) :

(nhds a).has_basis p (λ (i : ι), closure (s i))

theorem has_basis_nhds_closure {α : Type u} [topological_space α] [regular_space α] (a : α) :

(nhds a).has_basis (λ (s : set α), s ∈ nhds a) closure

theorem has_basis_opens_closure {α : Type u} [topological_space α] [regular_space α] (a : α) :

(nhds a).has_basis (λ (s : set α), a ∈ s ∧ is_open s) closure

theorem topological_space.is_topological_basis.nhds_basis_closure {α : Type u} [topological_space α] [regular_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) (a : α) :

(nhds a).has_basis (λ (s : set α), a ∈ s ∧ s ∈ B) closure

theorem topological_space.is_topological_basis.exists_closure_subset {α : Type u} [topological_space α] [regular_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {a : α} {s : set α} (h : s ∈ nhds a) :

∃ (t : set α) (H : t ∈ B), a ∈ t ∧ closure t ⊆ s

theorem disjoint_nhds_nhds_iff_not_specializes {α : Type u} [topological_space α] [regular_space α] {a b : α} :

disjoint (nhds a) (nhds b) ↔ ¬a ⤳ b

theorem specializes_comm {α : Type u} [topological_space α] [regular_space α] {a b : α} :

a ⤳ b ↔ b ⤳ a

theorem specializes.symm {α : Type u} [topological_space α] [regular_space α] {a b : α} :

a ⤳ b → b ⤳ a

Alias of the forward direction of specializes_comm.

theorem specializes_iff_inseparable {α : Type u} [topological_space α] [regular_space α] {a b : α} :

a ⤳ b ↔ inseparable a b

theorem is_closed_set_of_specializes {α : Type u} [topological_space α] [regular_space α] :

is_closed {p : α × α | p.fst ⤳ p.snd}

theorem is_closed_set_of_inseparable {α : Type u} [topological_space α] [regular_space α] :

is_closed {p : α × α | inseparable p.fst p.snd}

@[protected]

theorem inducing.regular_space {α : Type u} {β : Type v} [topological_space α] [regular_space α] [topological_space β] {f : β → α} (hf : inducing f) :

regular_space β

theorem regular_space_induced {α : Type u} {β : Type v} [topological_space α] [regular_space α] (f : β → α) :

regular_space β

theorem regular_space_Inf {X : Type u_1} {T : set (topological_space X)} (h : ∀ (t : topological_space X), t ∈ T → regular_space X) :

regular_space X

theorem regular_space_infi {ι : Sort u_1} {X : Type u_2} {t : ι → topological_space X} (h : ∀ (i : ι), regular_space X) :

regular_space X

theorem regular_space.inf {X : Type u_1} {t₁ t₂ : topological_space X} (h₁ : regular_space X) (h₂ : regular_space X) :

regular_space X

@[protected, instance]

def subtype.regular_space {α : Type u} [topological_space α] [regular_space α] {p : α → Prop} :

regular_space (subtype p)

@[protected, instance]

def prod.regular_space {α : Type u} {β : Type v} [topological_space α] [regular_space α] [topological_space β] [regular_space β] :

regular_space (α × β)

@[protected, instance]

def pi.regular_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), regular_space (π i)] :

regular_space (Π (i : ι), π i)

@[class]

structure t3_space (α : Type u) [topological_space α] :

Prop

to_t0_space : t0_space α
to_regular_space : regular_space α

A T₃ space is a T₀ space which is a regular space. Any T₃ space is a T₁ space, a T₂ space, and a T₂.₅ space.

Instances of this typeclass

@[protected, instance]

def t3_space.t2_5_space {α : Type u} [topological_space α] [t3_space α] :

t2_5_space α

@[protected]

theorem embedding.t3_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t3_space β] {f : α → β} (hf : embedding f) :

t3_space α

@[protected, instance]

def subtype.t3_space {α : Type u} [topological_space α] [t3_space α] {p : α → Prop} :

t3_space (subtype p)

@[protected, instance]

def prod.t3_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t3_space α] [t3_space β] :

t3_space (α × β)

@[protected, instance]

def pi.t3_space {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space (π i)] [∀ (i : ι), t3_space (π i)] :

t3_space (Π (i : ι), π i)

theorem disjoint_nested_nhds {α : Type u} [topological_space α] [t3_space α] {x y : α} (h : x ≠ y) :

∃ (U₁ : set α) (H : U₁ ∈ nhds x) (V₁ : set α) (H : V₁ ∈ nhds x) (U₂ : set α) (H : U₂ ∈ nhds y) (V₂ : set α) (H : V₂ ∈ nhds y), is_closed V₁ ∧ is_closed V₂ ∧ is_open U₁ ∧ is_open 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.

@[protected, instance]

def separation_quotient.t3_space {α : Type u} [topological_space α] [regular_space α] :

t3_space (separation_quotient α)

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

@[class]

structure normal_space (α : Type u) [topological_space α] :

Prop

to_t1_space : t1_space α
normal : ∀ (s t : set α), is_closed s → is_closed t → disjoint s t → separated_nhds s t

A T₄ space, also known as a normal space (although this condition sometimes omits T₂), is one in which for every pair of disjoint closed sets C and D, there exist disjoint open sets containing C and D respectively.

Instances of this typeclass

theorem normal_separation {α : Type u} [topological_space α] [normal_space α] {s t : set α} (H1 : is_closed s) (H2 : is_closed t) (H3 : disjoint s t) :

separated_nhds s t

theorem normal_exists_closure_subset {α : Type u} [topological_space α] [normal_space α] {s t : set α} (hs : is_closed s) (ht : is_open t) (hst : s ⊆ t) :

∃ (u : set α), is_open u ∧ s ⊆ u ∧ closure u ⊆ t

@[protected, instance]

def normal_space.t3_space {α : Type u} [topological_space α] [normal_space α] :

t3_space α

theorem normal_of_compact_t2 {α : Type u} [topological_space α] [compact_space α] [t2_space α] :

@[protected]

theorem closed_embedding.normal_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [normal_space β] {f : α → β} (hf : closed_embedding f) :

@[protected, instance]

def separation_quotient.normal_space {α : Type u} [topological_space α] [normal_space α] :

normal_space (separation_quotient α)

The separation_quotient of a normal space is a T₄ space. We don't have separate typeclasses for normal spaces (without T₁ assumption) and T₄ spaces, so we use the same class for assumption and for conclusion.

One can prove this using a homeomorphism between α and separation_quotient α. We give an alternative proof that works without assuming that α is a T₁ space.

theorem normal_space_of_t3_second_countable (α : Type u) [topological_space α] [topological_space.second_countable_topology α] [t3_space α] :

A T₃ topological space with second countable topology is a normal space. This lemma is not an instance to avoid a loop.

@[class]

structure t5_space (α : Type u) [topological_space α] :

Prop

to_t1_space : t1_space α
completely_normal : ∀ ⦃s t : set α⦄, disjoint (closure s) t → disjoint s (closure t) → disjoint (nhds_set s) (nhds_set t)

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.

Instances of this typeclass

theorem embedding.t5_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t5_space β] {e : α → β} (he : embedding e) :

t5_space α

@[protected, instance]

def subtype.t5_space {α : Type u} [topological_space α] [t5_space α] {p : α → Prop} :

t5_space {x // p x}

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

@[protected, instance]

def t5_space.to_normal_space {α : Type u} [topological_space α] [t5_space α] :

A T₅ space is a T₄ space.

@[protected, instance]

def separation_quotient.t5_space {α : Type u} [topological_space α] [t5_space α] :

t5_space (separation_quotient α)

The separation_quotient of a completely normal space is a T₅ space. We don't have separate typeclasses for completely normal spaces (without T₁ assumption) and T₅ spaces, so we use the same class for assumption and for conclusion.

One can prove this using a homeomorphism between α and separation_quotient α. We give an alternative proof that works without assuming that α is a T₁ space.

theorem connected_component_eq_Inter_clopen {α : Type u} [topological_space α] [t2_space α] [compact_space α] (x : α) :

connected_component x = ⋂ (Z : {Z // is_clopen Z ∧ x ∈ Z}), ↑Z

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

theorem totally_separated_space_of_t1_of_basis_clopen {α : Type u} [topological_space α] [t1_space α] (h : topological_space.is_topological_basis {s : set α | is_clopen s}) :

totally_separated_space α

A T1 space with a clopen basis is totally separated.

theorem compact_t2_tot_disc_iff_tot_sep {α : Type u} [topological_space α] [t2_space α] [compact_space α] :

totally_disconnected_space α ↔ totally_separated_space α

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

theorem nhds_basis_clopen {α : Type u} [topological_space α] [t2_space α] [compact_space α] [totally_disconnected_space α] (x : α) :

(nhds x).has_basis (λ (s : set α), x ∈ s ∧ is_clopen s) id

theorem is_topological_basis_clopen {α : Type u} [topological_space α] [t2_space α] [compact_space α] [totally_disconnected_space α] :

topological_space.is_topological_basis {s : set α | is_clopen s}

theorem compact_exists_clopen_in_open {α : Type u} [topological_space α] [t2_space α] [compact_space α] [totally_disconnected_space α] {x : α} {U : set α} (is_open : _root_.is_open U) (memU : x ∈ U) :

∃ (V : set α) (hV : is_clopen 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} [topological_space H] [locally_compact_space H] [t2_space H] [totally_disconnected_space H] :

topological_space.is_topological_basis {s : set H | is_clopen 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} [topological_space H] [locally_compact_space H] [t2_space H] :

totally_disconnected_space H ↔ totally_separated_space H

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