mathlib docs: topology.separation

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

source

theorem exists_open_singleton_of_open_finset {α : Type u} [topological_space α] [t0_space α] (s : finset α) (sne : s.nonempty) (hso : is_open ↑s) :

∃ (x : α) (H : x ∈ s), is_open {x}

source

theorem exists_open_singleton_of_fintype {α : Type u} [topological_space α] [t0_space α] [f : fintype α] [ha : nonempty α] :

∃ (x : α), is_open {x}

source

@[instance]

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

t0_space (subtype p)

source

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

source

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

is_closed {x}

source

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

is_open {x}ᶜ

source

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

is_open {y : α | y ≠ x}

source

@[instance]

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

t1_space (subtype p)

source

@[instance]

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

t0_space α

source

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

{x}ᶜ ∈ 𝓝 y

source

@[simp]

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

closure {a} = {a}

source

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

is_closed_map (function.const α y)

source

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

discrete_topology X

source

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

{x} ∈ 𝓝[s] x

source

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

𝓝[s] x = pure x

source

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 : (𝓝 x).has_basis p t) (hx : x ∈ s) :

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

source

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

source

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

∃ (U : set α) (H : U ∈ 𝓝[{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.

source

@[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 ∧ 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

source

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 ∧ u ∩ v = ∅

source

@[instance]

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

t1_space α

source

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

x = y

source

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

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

source

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

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

source

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

is_closed (set.diagonal α)

source

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

t2_space α ↔ is_closed (set.diagonal α)

source

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

disjoint s t → separated ↑s ↑t

source

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

separated {x} ↑s

source

@[simp]

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

𝓝 a = 𝓝 b ↔ a = b

source

@[simp]

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

𝓝 a ≤ 𝓝 b ↔ a = b

source

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 (𝓝 a)) (hb : filter.tendsto f l (𝓝 b)) :

a = b

source

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 (𝓝 a)) (hb : filter.tendsto f l (𝓝 b)) :

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.

source

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

Lim f = a

source

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

Lim f = a ↔ f ≤ 𝓝 a

source

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

F.Lim = x ↔ ↑F ≤ 𝓝 x

source

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

source

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 (𝓝 a)) :

lim f g = a

source

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 (𝓝 a)) {a : α} :

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

source

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

lim (𝓝 a) f = f a

source

@[simp]

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

Lim (𝓝 a) = a

source

@[simp]

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

lim (𝓝 a) id = a

source

@[simp]

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

Lim (𝓝[s] a) = a

source

@[simp]

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

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.

source

@[instance]

def t2_space_discrete {α : Type u_1} [topological_space α] [discrete_topology α] :

t2_space α

source

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 ∧ u ∩ v = ∅

source

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 ∧ u ∩ v = ∅

source

@[instance]

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

t2_space (subtype p)

source

@[instance]

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

t2_space (α × β)

source

@[instance]

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

t2_space (α ⊕ β)

source

@[instance]

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

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

source

@[instance]

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

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

source

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}

source

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.

source

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.

source

theorem diagonal_eq_range_diagonal_map {α : Type u_1} :

{p : α × α | p.fst = p.snd} = set.range (λ (x : α), (x, x))

source

theorem prod_subset_compl_diagonal_iff_disjoint {α : Type u_1} {s t : set α} :

s.prod t ⊆ {p : α × α | p.fst = p.snd}ᶜ ↔ s ∩ t = ∅

source

theorem compact_compact_separated {α : Type u} [topological_space α] [t2_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) (hst : s ∩ t = ∅) :

∃ (u v : set α), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u ∩ v = ∅

source

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.

source

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)

source

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.

source

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

source

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

locally_compact_space α

source

@[instance]

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

locally_compact_space α

source

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

source

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

∃ (K' : set α), is_compact K' ∧ K ⊆ interior K'

In a locally compact T₂ space, every compact set is contained in the interior of a compact set.

source

@[class]

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

Prop

to_t1_space : t1_space α
regular : ∀ {s : set α} {a : α}, is_closed s → a ∉ s → (∃ (t : set α), is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥)

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

source

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

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

source

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

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

source

@[instance]

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

regular_space (subtype p)

source

@[instance]

def regular_space.t2_space (α : Type u) [topological_space α] [regular_space α] :

t2_space α

source

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

∃ (U₁ V₁ : set α) (H : U₁ ∈ 𝓝 x) (H : V₁ ∈ 𝓝 x) (U₂ V₂ : set α) (H : U₂ ∈ 𝓝 y) (H : V₂ ∈ 𝓝 y), is_closed V₁ ∧ is_closed V₂ ∧ is_open U₁ ∧ is_open U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ U₁ ∩ U₂ = ∅

source

@[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 → (∃ (u v : set α), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ disjoint u v)

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.

source

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

source

@[instance]

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

regular_space α

source

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

normal_space α

source

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.

Properties of Lim and lim

Instances of t2_space typeclass

Properties of `Lim` and `lim`

Instances of `t2_space` typeclass