mathlib documentation

topology.bases

Bases of topologies. Countability axioms. #

A topological basis on a topological space t is a collection of sets, such that all open sets can be generated as unions of these sets, without the need to take finite intersections of them. This file introduces a framework for dealing with these collections, and also what more we can say under certain countability conditions on bases, which are referred to as first- and second-countable. We also briefly cover the theory of separable spaces, which are those with a countable, dense subset. If a space is second-countable, and also has a countably generated uniformity filter (for example, if t is a metric space), it will automatically be separable (and indeed, these conditions are equivalent in this case).

Main definitions #

Main results #

Implementation Notes #

For our applications we are interested that there exists a countable basis, but we do not need the concrete basis itself. This allows us to declare these type classes as Prop to use them as mixins.

TODO: #

More fine grained instances for first_countable_topology, separable_space, t2_space, and more (see the comment below subtype.second_countable_topology.)

structure topological_space.is_topological_basis {α : Type u} [t : topological_space α] (s : set (set α)) :
Prop

A topological basis is one that satisfies the necessary conditions so that it suffices to take unions of the basis sets to get a topology (without taking finite intersections as well).

If a family of sets s generates the topology, then intersections of finite subcollections of s form a topological basis.

theorem topological_space.is_topological_basis_of_open_of_nhds {α : Type u} [t : topological_space α] {s : set (set α)} (h_open : (u : set α), u s is_open u) (h_nhds : (a : α) (u : set α), a u is_open u ( (v : set α) (H : v s), a v v u)) :

If a family of open sets s is such that every open neighbourhood contains some member of s, then s is a topological basis.

theorem topological_space.is_topological_basis.mem_nhds_iff {α : Type u} [t : topological_space α] {a : α} {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) :
s nhds a (t : set α) (H : t b), a t t s

A set s is in the neighbourhood of a iff there is some basis set t, which contains a and is itself contained in s.

theorem topological_space.is_topological_basis.is_open_iff {α : Type u} [t : topological_space α] {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) :
is_open s (a : α), a s ( (t : set α) (H : t b), a t t s)
theorem topological_space.is_topological_basis.nhds_has_basis {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {a : α} :
(nhds a).has_basis (λ (t : set α), t b a t) (λ (t : set α), t)
@[protected]
@[protected]
theorem topological_space.is_topological_basis.mem_nhds {α : Type u} [t : topological_space α] {a : α} {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) (hs : s b) (ha : a s) :
s nhds a
theorem topological_space.is_topological_basis.exists_subset_of_mem_open {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {a : α} {u : set α} (au : a u) (ou : is_open u) :
(v : set α) (H : v b), a v v u
theorem topological_space.is_topological_basis.open_eq_sUnion' {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} (ou : is_open u) :
u = ⋃₀ {s ∈ B | s u}

Any open set is the union of the basis sets contained in it.

theorem topological_space.is_topological_basis.open_eq_sUnion {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} (ou : is_open u) :
(S : set (set α)) (H : S B), u = ⋃₀ S
theorem topological_space.is_topological_basis.open_eq_Union {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} (ou : is_open u) :
(β : Type u) (f : β set α), (u = (i : β), f i) (i : β), f i B
theorem topological_space.is_topological_basis.mem_closure_iff {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {s : set α} {a : α} :
a closure s (o : set α), o b a o (o s).nonempty

A point a is in the closure of s iff all basis sets containing a intersect s.

A set is dense iff it has non-trivial intersection with all basis sets.

theorem topological_space.is_topological_basis.exists_nonempty_subset {α : Type u} [t : topological_space α] {B : set (set α)} (hb : topological_space.is_topological_basis B) {u : set α} (hu : u.nonempty) (ou : is_open u) :
(v : set α) (H : v B), v.nonempty v u
theorem topological_space.is_topological_basis_of_cover {α : Type u} [t : topological_space α] {ι : Sort u_1} {U : ι set α} (Uo : (i : ι), is_open (U i)) (Uc : ( (i : ι), U i) = set.univ) {b : Π (i : ι), set (set (U i))} (hb : (i : ι), topological_space.is_topological_basis (b i)) :
@[protected]
theorem topological_space.is_topological_basis.continuous {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] {B : set (set β)} (hB : topological_space.is_topological_basis B) (f : α β) (hf : (s : set β), s B is_open (f ⁻¹' s)) :
@[class]
structure topological_space.separable_space (α : Type u) [t : topological_space α] :
Prop

A separable space is one with a countable dense subset, available through topological_space.exists_countable_dense. If α is also known to be nonempty, then topological_space.dense_seq provides a sequence ℕ → α with dense range, see topological_space.dense_range_dense_seq.

If α is a uniform space with countably generated uniformity filter (e.g., an emetric_space), then this condition is equivalent to topological_space.second_countable_topology α. In this case the latter should be used as a typeclass argument in theorems because Lean can automatically deduce separable_space from second_countable_topology but it can't deduce second_countable_topology and emetric_space.

Instances of this typeclass

A nonempty separable space admits a sequence with dense range. Instead of running cases on the conclusion of this lemma, you might want to use topological_space.dense_seq and topological_space.dense_range_dense_seq.

If α might be empty, then exists_countable_dense is the main way to use separability of α.

A dense sequence in a non-empty separable topological space.

If α might be empty, then exists_countable_dense is the main way to use separability of α.

Equations
@[simp]

The sequence dense_seq α has dense range.

theorem set.pairwise_disjoint.countable_of_is_open {α : Type u} [t : topological_space α] [topological_space.separable_space α] {ι : Type u_1} {s : ι set α} {a : set ι} (h : a.pairwise_disjoint s) (ha : (i : ι), i a is_open (s i)) (h'a : (i : ι), i a (s i).nonempty) :

In a separable space, a family of nonempty disjoint open sets is countable.

theorem set.pairwise_disjoint.countable_of_nonempty_interior {α : Type u} [t : topological_space α] [topological_space.separable_space α] {ι : Type u_1} {s : ι set α} {a : set ι} (h : a.pairwise_disjoint s) (ha : (i : ι), i a (interior (s i)).nonempty) :

In a separable space, a family of disjoint sets with nonempty interiors is countable.

def topological_space.is_separable {α : Type u} [t : topological_space α] (s : set α) :
Prop

A set s in a topological space is separable if it is contained in the closure of a countable set c. Beware that this definition does not require that c is contained in s (to express the latter, use separable_space s or is_separable (univ : set s)). In metric spaces, the two definitions are equivalent, see topological_space.is_separable.separable_space.

Equations
theorem topological_space.is_separable_Union {α : Type u} [t : topological_space α] {ι : Type u_1} [countable ι] {s : ι set α} (hs : (i : ι), topological_space.is_separable (s i)) :
theorem is_topological_basis_pi {ι : Type u_1} {X : ι Type u_2} [Π (i : ι), topological_space (X i)] {T : Π (i : ι), set (set (X i))} (cond : (i : ι), topological_space.is_topological_basis (T i)) :
topological_space.is_topological_basis {S : set (Π (i : ι), X i) | (U : Π (i : ι), set (X i)) (F : finset ι), ( (i : ι), i F U i T i) S = F.pi U}
theorem is_topological_basis_infi {β : Type u_1} {ι : Type u_2} {X : ι Type u_3} [t : Π (i : ι), topological_space (X i)] {T : Π (i : ι), set (set (X i))} (cond : (i : ι), topological_space.is_topological_basis (T i)) (f : Π (i : ι), β X i) :
topological_space.is_topological_basis {S : set β | (U : Π (i : ι), set (X i)) (F : finset ι), ( (i : ι), i F U i T i) S = (i : ι) (hi : i F), f i ⁻¹' U i}
@[protected]

If α is a separable space and f : α → β is a continuous map with dense range, then β is a separable space as well. E.g., the completion of a separable uniform space is separable.

theorem dense.exists_countable_dense_subset_bot_top {α : Type u_1} [topological_space α] [partial_order α] {s : set α} [topological_space.separable_space s] (hs : dense s) :
(t : set α) (H : t s), t.countable dense t ( (x : α), is_bot x x s x t) (x : α), is_top x x s x t

Let s be a dense set in a topological space α with partial order structure. If s is a separable space (e.g., if α has a second countable topology), then there exists a countable dense subset t ⊆ s such that t contains bottom/top element of α when they exist and belong to s. For a dense subset containing neither bot nor top elements, see dense.exists_countable_dense_subset_no_bot_top.

theorem exists_countable_dense_bot_top (α : Type u_1) [topological_space α] [topological_space.separable_space α] [partial_order α] :
(s : set α), s.countable dense s ( (x : α), is_bot x x s) (x : α), is_top x x s

If α is a separable topological space with a partial order, then there exists a countable dense set s : set α that contains those of both bottom and top elements of α that actually exist. For a dense set containing neither bot nor top elements, see exists_countable_dense_no_bot_top.

In a first-countable space, a cluster point x of a sequence is the limit of some subsequence.

@[protected, instance]

A countable topological basis of α.

Equations
Instances for topological_space.countable_basis

If β is a second-countable space, then its induced topology via f on α is also second-countable.

@[protected, instance]

A countable open cover induces a second-countable topology if all open covers are themselves second countable.

theorem topological_space.is_open_Union_countable {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {ι : Type u_1} (s : ι set α) (H : (i : ι), is_open (s i)) :
(T : set ι), T.countable ( (i : ι) (H : i T), s i) = (i : ι), s i

In a second-countable space, an open set, given as a union of open sets, is equal to the union of countably many of those sets.

theorem topological_space.countable_cover_nhds {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {f : α set α} (hf : (x : α), f x nhds x) :
(s : set α), s.countable ( (x : α) (H : x s), f x) = set.univ

In a topological space with second countable topology, if f is a function that sends each point x to a neighborhood of x, then for some countable set s, the neighborhoods f x, x ∈ s, cover the whole space.

theorem topological_space.countable_cover_nhds_within {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {f : α set α} {s : set α} (hf : (x : α), x s f x nhds_within x s) :
(t : set α) (H : t s), t.countable s (x : α) (H : x t), f x
theorem topological_space.is_topological_basis.sigma {ι : Type u_1} {E : ι Type u_2} [Π (i : ι), topological_space (E i)] {s : Π (i : ι), set (set (E i))} (hs : (i : ι), topological_space.is_topological_basis (s i)) :
topological_space.is_topological_basis ( (i : ι), (λ (u : set (E i)), sigma.mk i '' u) '' s i)

In a disjoint union space Σ i, E i, one can form a topological basis by taking the union of topological bases on each of the parts of the space.

@[protected, instance]

A countable disjoint union of second countable spaces is second countable.

In a sum space α ⊕ β, one can form a topological basis by taking the union of topological bases on each of the two components.

@[protected, instance]

A sum type of two second countable spaces is second countable.

The image of a topological basis under an open quotient map is a topological basis.

A second countable space is mapped by an open quotient map to a second countable space.

The image of a topological basis "downstairs" in an open quotient is a topological basis.