mathlib documentation

topology.separation

Separation properties of topological spaces. #

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

Main definitions #

Main results #

T₀ spaces #

T₁ spaces #

T₂ spaces #

If the space is also compact:

T₃ spaces #

Discrete spaces #

References #

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

def separated {α : Type u} [topological_space α] :
set αset α → Prop

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

Equations
@[symm]
theorem separated.symm {α : Type u} [topological_space α] {s t : set α} :
separated s tseparated t s
theorem separated.comm {α : Type u} [topological_space α] (s t : set α) :
theorem separated.preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} {s t : set β} (h : separated s t) (hf : continuous f) :
separated (f ⁻¹' s) (f ⁻¹' t)
@[protected]
theorem separated.disjoint {α : Type u} [topological_space α] {s t : set α} (h : separated s t) :
theorem separated.disjoint_closure_left {α : Type u} [topological_space α] {s t : set α} (h : separated s t) :
theorem separated.disjoint_closure_right {α : Type u} [topological_space α] {s t : set α} (h : separated s t) :
theorem separated.empty_right {α : Type u} [topological_space α] (a : set α) :
theorem separated.empty_left {α : Type u} [topological_space α] (a : set α) :
theorem separated.mono {α : Type u} [topological_space α] {s₁ s₂ t₁ t₂ : set α} (h : separated s₂ t₂) (hs : s₁ s₂) (ht : t₁ t₂) :
separated s₁ t₁
theorem separated.union_left {α : Type u} [topological_space α] {a b c : set α} :
separated a cseparated b cseparated (a b) c
theorem separated.union_right {α : Type u} [topological_space α] {a b c : set α} (ab : separated a b) (ac : separated a c) :
separated a (b c)
@[class]
structure t0_space (α : Type u) [topological_space α] :
Prop

A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair x ≠ y, there is an open set containing one but not the other. We formulate the definition in terms of the inseparable relation.

Instances of this typeclass
theorem t0_space_iff_inseparable (α : Type u) [topological_space α] :
t0_space α ∀ (x y : α), inseparable x yx = 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
@[simp]
theorem nhds_eq_nhds_iff {α : Type u} [topological_space α] [t0_space α] {a b : α} :
nhds a = nhds b a = b
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 α] :

Specialization forms a partial order on a t0 topological space.

Equations
@[protected, instance]
theorem minimal_nonempty_closed_subsingleton {α : Type u} [topological_space α] [t0_space α] {s : set α} (hs : is_closed s) (hmin : ∀ (t : set α), t st.nonemptyis_closed tt = s) :
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 st.nonemptyis_closed tt = 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 st.nonemptyis_open tt = s) :
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 st.nonemptyis_open tt = 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} :
theorem t0_space_iff_or_not_mem_closure (α : Type u) [topological_space α] :
t0_space α ∀ (a b : α), a ba 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

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 : α} :
theorem is_open_compl_singleton {α : Type u} [topological_space α] [t1_space α] {x : α} :
theorem is_open_ne {α : Type u} [topological_space α] [t1_space α] {x : α} :
is_open {y : α | y x}
theorem ne.nhds_within_compl_singleton {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x y) :
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
@[protected]
theorem set.finite.is_closed {α : Type u} [topological_space α] [t1_space α] {s : set α} (hs : s.finite) :
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

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
@[protected]
theorem finset.is_closed {α : Type u} [topological_space α] [t1_space α] (s : finset α) :
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 ydisjoint (nhds x) (has_pure.pure y), ∀ ⦃x y : α⦄, x ydisjoint (has_pure.pure x) (nhds y), ∀ ⦃x y : α⦄, x yx = y].tfae
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 ydisjoint (has_pure.pure x) (nhds y)
theorem t1_space_iff_disjoint_nhds_pure {α : Type u} [topological_space α] :
t1_space α ∀ ⦃x y : α⦄, x ydisjoint (nhds x) (has_pure.pure y)
theorem t1_space_iff_specializes_imp_eq {α : Type u} [topological_space α] :
t1_space α ∀ ⦃x y : α⦄, x yx = y
theorem disjoint_pure_nhds {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x y) :
theorem disjoint_nhds_pure {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x y) :
theorem specializes.eq {α : Type u} [topological_space α] [t1_space α] {x y : α} (h : x y) :
x = y
@[simp]
theorem specializes_iff_eq {α : Type u} [topological_space α] [t1_space α] {x y : α} :
x y x = y
@[protected, instance]
theorem t1_space_antitone {α : Type u_1} :
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) :
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) :
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 sfilter.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 β] :
@[protected]
theorem embedding.t1_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t1_space β] {f : α → β} (hf : embedding f) :
@[protected, instance]
def subtype.t1_space {α : Type u} [topological_space α] [t1_space α] {p : α → Prop} :
@[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) :
@[simp]
theorem subsingleton_closure {α : Type u} [topological_space α] [t1_space α] {s : set α} :
theorem is_closed_map_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] [t1_space β] {y : β} :
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 pure_le_nhds_iff {α : Type u} [topological_space α] [t1_space α] {a b : α} :
@[simp]
theorem nhds_le_nhds_iff {α : Type u} [topological_space α] [t1_space α] {a b : α} :
nhds a nhds b a = b
@[simp]
theorem compl_singleton_mem_nhds_set_iff {α : Type u} [topological_space α] [t1_space α] {x : α} {s : set α} :
@[simp]
theorem nhds_set_le_iff {α : Type u} [topological_space α] [t1_space α] {s t : set α} :
@[simp]
theorem nhds_set_inj_iff {α : Type u} [topological_space α] [t1_space α] {s t : set α} :
@[simp]
theorem nhds_le_nhds_set {α : Type u} [topological_space α] [t1_space α] {s : set α} {x : α} :
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 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)) :

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

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

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

The neighbourhoods filter of x within s, under the discrete topology, is equal to the pure x filter (which is the principal filter at the singleton {x}.)

theorem filter.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

  1. U is a punctured neighborhood of x (ie. U ∪ {x} is a neighbourhood of x),
  2. U is disjoint from 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.

This lemma characterizes discrete topological spaces as those whose singletons are neighbourhoods.

theorem induced_bot {X : Type u_1} {Y : Type u_2} {f : X → Y} (hf : function.injective 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) :

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

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

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.

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 ydisjoint (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 t2_separation_finset {α : Type u} [topological_space α] [t2_space α] (s : finset α) :
∃ (f : α → set α), s.pairwise_disjoint f ∀ (x : α), x sx f x is_open (f x)

A finite set can be separated by open sets.

@[protected, instance]
def t2_space.t1_space {α : Type u} [topological_space α] [t2_space α] :
theorem t2_iff_nhds {α : Type u} [topological_space α] :
t2_space α ∀ {x y : α}, (nhds x nhds y).ne_botx = 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 xf nhds yx = y
theorem is_closed_diagonal {α : Type u} [topological_space α] [t2_space α] :
theorem finset_disjoint_finset_opens_of_t2 {α : Type u} [topological_space α] [t2_space α] (s t : finset α) :
theorem point_disjoint_finset_opens_of_t2 {α : Type u} [topological_space α] [t2_space α] {x : α} {s : finset α} (h : 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

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
@[protected, instance]
def t2_5_space.t2_space {α : Type u} [topological_space α] [t2_5_space α] :

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 UU 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) :

t2_space constructions #

We use two lemmas to prove that various standard constructions generate Hausdorff spaces from Hausdorff spaces:

@[protected, instance]
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 α] :
@[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) :
@[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) :

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 tf 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 tf 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) :
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) :
theorem compact_compact_separated {α : Type u} [topological_space α] [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : disjoint s t) :
∃ (u v : set α), is_open u is_open v s u t v disjoint u v
theorem is_compact.is_closed {α : Type u} [topological_space α] [t2_space α] {s : set α} (hs : is_compact s) :

In a t2_space, every compact set is closed.

theorem exists_subset_nhd_of_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 : ) :
theorem is_compact.inter {α : Type u} [topological_space α] [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :
theorem compact_closure_of_subset_compact {α : Type u} [topological_space α] [t2_space α] {s t : set α} (ht : is_compact t) (h : s t) :
@[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_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) :
theorem continuous.closed_embedding {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [t2_space β] {f : α → β} (h : continuous f) (hf : function.injective 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 tis_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) :
@[protected, instance]
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_irreducible_iff_singleton {α : Type u} [topological_space α] [t2_space α] (S : set α) :
is_irreducible S ∃ (x : α), S = {x}
@[class]
structure t3_space (α : Type u) [topological_space α] :
Prop

A T₃ space is a T₀ space in which for every closed C and x ∉ C, there exist disjoint open sets containing x and C respectively.

Instances of this typeclass
@[protected, instance]
def t3_space.t1_space {α : Type u} [topological_space α] [t3_space α] :
theorem nhds_is_closed {α : Type u} [topological_space α] [t3_space α] {a : α} {s : set α} (h : s nhds a) :
∃ (t : set α) (H : t nhds a), t s is_closed t
theorem closed_nhds_basis {α : Type u} [topological_space α] [t3_space α] (a : α) :
(nhds a).has_basis (λ (s : set α), s nhds a is_closed s) id
theorem topological_space.is_topological_basis.exists_closure_subset {α : Type u} [topological_space α] [t3_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
@[protected]
theorem embedding.t3_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [t3_space β] {f : α → β} (hf : embedding f) :
@[protected, instance]
def subtype.t3_space {α : Type u} [topological_space α] [t3_space α] {p : α → Prop} :
@[protected, instance]
def t3_space.t2_space (α : Type u) [topological_space α] [t3_space α] :
@[protected, instance]
def t3_space.t2_5_space (α : Type u) [topological_space α] [t3_space α] :
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.

@[class]
structure normal_space (α : Type u) [topological_space α] :
Prop

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) :
∃ (u v : set α), is_open u is_open v s u t v disjoint u v
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 α] :
@[protected]
theorem closed_embedding.normal_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [normal_space β] {f : α → β} (hf : closed_embedding f) :

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

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.

A Hausdorff space with a clopen basis is totally separated.

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

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

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

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

@[protected, instance]

connected_components α is Hausdorff when α is Hausdorff and compact