# mathlibdocumentation

topology.separation

def separated {α : Type u}  :
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
theorem separated.symm {α : Type u} {s t : set α} :
t s
theorem separated.comm {α : Type u} (s t : set α) :
t s
theorem separated.empty_right {α : Type u} (a : set α) :
theorem separated.empty_left {α : Type u} (a : set α) :
theorem separated.union_left {α : Type u} {a b c : set α} :
c cseparated (a b) c
theorem separated.union_right {α : Type u} {a b c : set α} (ab : b) (ac : c) :
(b c)
@[class]
structure t0_space (α : Type u)  :
Prop

A T₀ space, also known as a Kolmogorov space, is a topological space where for every pair x ≠ y, there is an open set containing one but not the other.

Instances
theorem is_closed.exists_closed_singleton {α : Type u_1} [t0_space α] {S : set α} (hS : is_closed S) (hne : S.nonempty) :
∃ (x : α), x S is_closed {x}
theorem exists_open_singleton_of_open_finset {α : Type u} [t0_space α] (s : finset α) (sne : s.nonempty) (hso : is_open s) :
∃ (x : α) (H : x s), is_open {x}
theorem exists_open_singleton_of_fintype {α : Type u} [t0_space α] [f : fintype α] [ha : nonempty α] :
∃ (x : α), is_open {x}
@[instance]
def subtype.t0_space {α : Type u} [t0_space α] {p : α → Prop} :
@[class]
structure t1_space (α : Type u)  :
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
theorem is_closed_singleton {α : Type u} [t1_space α] {x : α} :
theorem is_open_compl_singleton {α : Type u} [t1_space α] {x : α} :
theorem is_open_ne {α : Type u} [t1_space α] {x : α} :
is_open {y : α | y x}
@[instance]
def subtype.t1_space {α : Type u} [t1_space α] {p : α → Prop} :
@[instance]
def t1_space.t0_space {α : Type u} [t1_space α] :
theorem compl_singleton_mem_nhds {α : Type u} [t1_space α] {x y : α} (h : y x) :
{x} 𝓝 y
@[simp]
theorem closure_singleton {α : Type u} [t1_space α] {a : α} :
closure {a} = {a}
theorem set.subsingleton.closure {α : Type u} [t1_space α] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem subsingleton_closure {α : Type u} [t1_space α] {s : set α} :
theorem is_closed_map_const {α : Type u_1} {β : Type u_2} [t1_space β] {y : β} :
theorem discrete_of_t1_of_finite {X : Type u_1} [t1_space X] [fintype X] :
theorem singleton_mem_nhds_within_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
{x} 𝓝[s] x
theorem nhds_within_of_mem_discrete {α : Type u} {s : set α} {x : α} (hx : x s) :
theorem filter.has_basis.exists_inter_eq_singleton_of_mem_discrete {α : Type u} {ι : Type u_1} {p : ι → Prop} {t : ι → set α} {s : set α} {x : α} (hb : (𝓝 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} {s : set α} {x : α} (hx : x s) :
∃ (U : set α) (H : U 𝓝 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} {s : set α} {x : α} (hx : x s) :
∃ (U : set α) (H : U 𝓝[{x}] x), s

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

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

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] {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} {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.

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

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

Instances
theorem t2_separation {α : Type u} [t2_space α] {x y : α} (h : x y) :
∃ (u v : set α), x u y v u v =
@[instance]
def t2_space.t1_space {α : Type u} [t2_space α] :
theorem eq_of_nhds_ne_bot {α : Type u} [ht : t2_space α] {x y : α} (h : (𝓝 x 𝓝 y).ne_bot) :
x = y
theorem t2_iff_nhds {α : Type u}  :
∀ {x y : α}, (𝓝 x 𝓝 y).ne_botx = y
theorem t2_iff_ultrafilter {α : Type u}  :
∀ {x y : α} (f : , f 𝓝 xf 𝓝 yx = y
theorem is_closed_diagonal {α : Type u} [t2_space α] :
theorem t2_iff_is_closed_diagonal {α : Type u}  :
theorem finset_disjoint_finset_opens_of_t2 {α : Type u} [t2_space α] (s t : finset α) :
t t
theorem point_disjoint_finset_opens_of_t2 {α : Type u} [t2_space α] {x : α} {s : finset α} (h : x s) :
@[simp]
theorem nhds_eq_nhds_iff {α : Type u} {a b : α} [t2_space α] :
𝓝 a = 𝓝 b a = b
@[simp]
theorem nhds_le_nhds_iff {α : Type u} {a b : α} [t2_space α] :
𝓝 a 𝓝 b a = b
theorem tendsto_nhds_unique {α : Type u} {β : Type v} [t2_space α] {f : β → α} {l : filter β} {a b : α} [l.ne_bot] (ha : (𝓝 a)) (hb : (𝓝 b)) :
a = b
theorem tendsto_nhds_unique' {α : Type u} {β : Type v} [t2_space α] {f : β → α} {l : filter β} {a b : α} (hl : l.ne_bot) (ha : (𝓝 a)) (hb : (𝓝 b)) :
a = b
theorem tendsto_nhds_unique_of_eventually_eq {α : Type u} {β : Type v} [t2_space α] {f g : β → α} {l : filter β} {a b : α} [l.ne_bot] (ha : (𝓝 a)) (hb : (𝓝 b)) (hfg : f =ᶠ[l] g) :
a = b

### 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} [t2_space α] {f : filter α} {a : α} [f.ne_bot] (h : f 𝓝 a) :
Lim f = a
theorem Lim_eq_iff {α : Type u} [t2_space α] {f : filter α} [f.ne_bot] (h : ∃ (a : α), f 𝓝 a) {a : α} :
Lim f = a f 𝓝 a
theorem ultrafilter.Lim_eq_iff_le_nhds {α : Type u} [t2_space α] {x : α} {F : ultrafilter α} :
F.Lim = x F 𝓝 x
theorem is_open_iff_ultrafilter' {α : Type u} [t2_space α] (U : set α) :
∀ (F : , F.Lim UU F.to_filter
theorem filter.tendsto.lim_eq {α : Type u} {β : Type v} [t2_space α] {a : α} {f : filter β} [f.ne_bot] {g : β → α} (h : (𝓝 a)) :
lim f g = a
theorem filter.lim_eq_iff {α : Type u} {β : Type v} [t2_space α] {f : filter β} [f.ne_bot] {g : β → α} (h : ∃ (a : α), (𝓝 a)) {a : α} :
lim f g = a (𝓝 a)
theorem continuous.lim_eq {α : Type u} {β : Type v} [t2_space α] {f : β → α} (h : continuous f) (a : β) :
lim (𝓝 a) f = f a
@[simp]
theorem Lim_nhds {α : Type u} [t2_space α] (a : α) :
Lim (𝓝 a) = a
@[simp]
theorem lim_nhds_id {α : Type u} [t2_space α] (a : α) :
lim (𝓝 a) id = a
@[simp]
theorem Lim_nhds_within {α : Type u} [t2_space α] {a : α} {s : set α} (h : a ) :
Lim (𝓝[s] a) = a
@[simp]
theorem lim_nhds_within_id {α : Type u} [t2_space α] {a : α} {s : set α} (h : a ) :
lim (𝓝[s] a) id = a

### Instances of t2_space typeclass #

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 thatf x ≠ f y. We use this lemma to prove that topological spaces defined usinginduced 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.

@[instance]
def t2_space_discrete {α : Type u_1}  :
theorem separated_by_continuous {α : Type u_1} {β : Type u_2} [t2_space β] {f : α → β} (hf : continuous f) {x y : α} (h : f x f y) :
∃ (u v : set α), x u y v u v =
theorem separated_by_open_embedding {α : Type u_1} {β : Type u_2} [t2_space α] {f : α → β} (hf : open_embedding f) {x y : α} (h : x y) :
∃ (u v : set β), f x u f y v u v =
@[instance]
def subtype.t2_space {α : Type u_1} {p : α → Prop} [t : topological_space α] [t2_space α] :
@[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} [t2_space β] {f : α → β} (hf : embedding f) :
@[instance]
def sum.t2_space {α : Type u_1} {β : Type u_2} [t₁ : topological_space α] [t2_space α] [t₂ : topological_space β] [t2_space β] :
t2_space β)
@[instance]
def Pi.t2_space {α : Type u_1} {β : α → Type v} [t₂ : Π (a : α), topological_space (β a)] [∀ (a : α), t2_space (β a)] :
t2_space (Π (a : α), β a)
@[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} [t2_space α] {f g : β → α} (hf : continuous f) (hg : continuous g) :
is_closed {x : β | f x = g x}
theorem set.eq_on.closure {α : Type u} {β : Type v} [t2_space α] {s : set β} {f g : β → α} (h : g s) (hf : continuous f) (hg : continuous g) :
g (closure s)

If two continuous maps are equal on s, then they are equal on the closure of s.

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

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

theorem function.left_inverse.closed_range {α : Type u} {β : Type v} [t2_space α] {f : α → β} {g : β → α} (h : g) (hf : continuous f) (hg : continuous g) :
theorem function.left_inverse.closed_embedding {α : Type u} {β : Type v} [t2_space α] {f : α → β} {g : β → α} (h : g) (hf : continuous f) (hg : continuous g) :
theorem diagonal_eq_range_diagonal_map {α : Type u_1} :
{p : α × α | p.fst = p.snd} = set.range (λ (x : α), (x, x))
theorem prod_subset_compl_diagonal_iff_disjoint {α : Type u_1} {s t : set α} :
s.prod t {p : α × α | p.fst = p.snd} s t =
theorem compact_compact_separated {α : Type u} [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : s t = ) :
∃ (u v : set α), s u t v u v =
theorem is_compact.is_closed {α : Type u} [t2_space α] {s : set α} (hs : is_compact s) :

In a t2_space, every compact set is closed.

theorem compact_exhaustion.is_closed {α : Type u} [t2_space α] (K : compact_exhaustion α) (n : ) :
theorem is_compact.inter {α : Type u} [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :
theorem compact_closure_of_subset_compact {α : Type u} [t2_space α] {s t : set α} (ht : is_compact t) (h : s t) :
theorem image_closure_of_compact {α : Type u} {β : Type v} [t2_space β] {s : set α} (hs : is_compact (closure s)) {f : α → β} (hf : (closure s)) :
f '' = closure (f '' s)
theorem is_compact.binary_compact_cover {α : Type u} [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 α), 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} [t2_space β] {f : α → β} (h : continuous f) :
theorem continuous.closed_embedding {α : Type u} {β : Type v} [t2_space β] {f : α → β} (h : continuous f) (hf : function.injective f) :
theorem is_compact.finite_compact_cover {α : Type u} [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} [t2_space α] (h : ∀ (x : α), ∃ (s : set α), s 𝓝 x ) :
@[instance]
def locally_compact_of_compact {α : Type u} [t2_space α]  :
theorem exists_open_with_compact_closure {α : Type u} [t2_space α] (x : α) :
∃ (U : set α), x U

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

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

A T₃ space, also known as a regular space (although this condition sometimes omits T₂), is one in which for every closed C and x ∉ C, there exist disjoint open sets containing x and C respectively.

Instances
theorem nhds_is_closed {α : Type u} {a : α} {s : set α} (h : s 𝓝 a) :
∃ (t : set α) (H : t 𝓝 a), t s
theorem closed_nhds_basis {α : Type u} (a : α) :
(𝓝 a).has_basis (λ (s : set α), s 𝓝 a id
@[instance]
def subtype.regular_space {α : Type u} {p : α → Prop} :
@[instance]
def regular_space.t2_space (α : Type u)  :
theorem disjoint_nested_nhds {α : Type u} {x y : α} (h : x y) :
∃ (U₁ V₁ : set α) (H : U₁ 𝓝 x) (H : V₁ 𝓝 x) (U₂ V₂ : set α) (H : U₂ 𝓝 y) (H : V₂ 𝓝 y), is_open U₁ is_open U₂ V₁ U₁ V₂ U₂ U₁ U₂ =
@[class]
structure normal_space (α : Type u)  :
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
theorem normal_separation {α : Type u} [normal_space α] {s t : set α} (H1 : is_closed s) (H2 : is_closed t) (H3 : t) :
∃ (u v : set α), s u t v v
theorem normal_exists_closure_subset {α : Type u} [normal_space α] {s t : set α} (hs : is_closed s) (ht : is_open t) (hst : s t) :
∃ (u : set α), s u t
@[instance]
def normal_space.regular_space {α : Type u} [normal_space α] :
theorem normal_of_compact_t2 {α : Type u} [t2_space α] :
theorem connected_component_eq_Inter_clopen {α : Type u} [t2_space α] {x : α} :
= ⋂ (Z : {Z // x Z}), Z

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

@[instance]
def connected_components.t2 {α : Type u} [t2_space α]  :

connected_components α is Hausdorff when α` is Hausdorff and compact