mathlib3 documentation

topology.bases

Bases of topologies. Countability axioms. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

is_topological_basis s: The topological space t has basis s.
separable_space α: The topological space t has a countable, dense subset.
is_separable s: The set s is contained in the closure of a countable set.
first_countable_topology α: A topology in which 𝓝 x is countably generated for every x.
second_countable_topology α: A topology which has a topological basis which is countable.

Main results #

first_countable_topology.tendsto_subseq: In a first-countable space, cluster points are limits of subsequences.
second_countable_topology.is_open_Union_countable: In a second-countable space, the union of arbitrarily-many open sets is equal to a sub-union of only countably many of these sets.
second_countable_topology.countable_cover_nhds: Consider f : α → set α with the property that f x ∈ 𝓝 x for all x. Then there is some countable set s whose image covers the space.

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

exists_subset_inter : ∀ (t₁ : set α), t₁ ∈ s → ∀ (t₂ : set α), t₂ ∈ s → ∀ (x : α), x ∈ t₁ ∩ t₂ → (∃ (t₃ : set α) (H : t₃ ∈ s), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂)
sUnion_eq : ⋃₀ s = set.univ
eq_generate_from : t = topological_space.generate_from s

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

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

topological_space.is_topological_basis (has_insert.insert ∅ s)

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

topological_space.is_topological_basis (s \ {∅})

theorem topological_space.is_topological_basis_of_subbasis {α : Type u} [t : topological_space α] {s : set (set α)} (hs : t = topological_space.generate_from s) :

topological_space.is_topological_basis ((λ (f : set (set α)), ⋂₀ f) '' {f : set (set α) | f.finite ∧ f ⊆ s})

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

topological_space.is_topological_basis s

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]

theorem topological_space.is_topological_basis.is_open {α : Type u} [t : topological_space α] {s : set α} {b : set (set α)} (hb : topological_space.is_topological_basis b) (hs : s ∈ b) :

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

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_iff_eq_sUnion {α : Type u} [t : topological_space α] {B : set (set α)} (hB : topological_space.is_topological_basis B) {u : set α} :

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.

theorem topological_space.is_topological_basis.dense_iff {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) {s : set α} :

dense s ↔ ∀ (o : set α), o ∈ b → o.nonempty → (o ∩ s).nonempty

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

theorem topological_space.is_topological_basis.is_open_map_iff {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] {B : set (set α)} (hB : topological_space.is_topological_basis B) {f : α → β} :

is_open_map f ↔ ∀ (s : set α), s ∈ B → is_open (f '' s)

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_opens {α : Type u} [t : topological_space α] :

topological_space.is_topological_basis {U : set α | is_open U}

@[protected]

theorem topological_space.is_topological_basis.prod {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] {B₁ : set (set α)} {B₂ : set (set β)} (h₁ : topological_space.is_topological_basis B₁) (h₂ : topological_space.is_topological_basis B₂) :

topological_space.is_topological_basis (set.image2 set.prod B₁ B₂)

@[protected]

theorem topological_space.is_topological_basis.inducing {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] {f : α → β} {T : set (set β)} (hf : inducing f) (h : topological_space.is_topological_basis T) :

topological_space.is_topological_basis (set.preimage f '' T)

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

topological_space.is_topological_basis (⋃ (i : ι), set.image coe '' 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

exists_countable_dense : ∃ (s : set α), s.countable ∧ dense s

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

theorem topological_space.exists_countable_dense (α : Type u) [t : topological_space α] [topological_space.separable_space α] :

∃ (s : set α), s.countable ∧ dense s

theorem topological_space.exists_dense_seq (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] :

∃ (u : ℕ → α), dense_range u

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

noncomputable def topological_space.dense_seq (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] :

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

topological_space.dense_seq α = classical.some _

@[simp]

theorem topological_space.dense_range_dense_seq (α : Type u) [t : topological_space α] [topological_space.separable_space α] [nonempty α] :

dense_range (topological_space.dense_seq α)

The sequence dense_seq α has dense range.

@[protected, instance]

def topological_space.countable.to_separable_space {α : Type u} [t : topological_space α] [countable α] :

topological_space.separable_space α

theorem topological_space.separable_space_of_dense_range {α : Type u} [t : topological_space α] {ι : Type u_1} [countable ι] (u : ι → α) (hu : dense_range u) :

topological_space.separable_space α

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

topological_space.is_separable s = ∃ (c : set α), c.countable ∧ s ⊆ closure c

theorem topological_space.is_separable.mono {α : Type u} [t : topological_space α] {s u : set α} (hs : topological_space.is_separable s) (hu : u ⊆ s) :

topological_space.is_separable u

theorem topological_space.is_separable.union {α : Type u} [t : topological_space α] {s u : set α} (hs : topological_space.is_separable s) (hu : topological_space.is_separable u) :

topological_space.is_separable (s ∪ u)

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

topological_space.is_separable (closure s)

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

topological_space.is_separable (⋃ (i : ι), s i)

theorem set.countable.is_separable {α : Type u} [t : topological_space α] {s : set α} (hs : s.countable) :

topological_space.is_separable s

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

topological_space.is_separable s

theorem topological_space.is_separable_univ_iff {α : Type u} [t : topological_space α] :

topological_space.is_separable set.univ ↔ topological_space.separable_space α

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

topological_space.is_separable s

theorem topological_space.is_separable.image {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] {s : set α} (hs : topological_space.is_separable s) {f : α → β} (hf : continuous f) :

topological_space.is_separable (f '' s)

theorem topological_space.is_separable_of_separable_space_subtype {α : Type u} [t : topological_space α] (s : set α) [topological_space.separable_space ↥s] :

topological_space.is_separable s

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}

theorem is_topological_basis_singletons (α : Type u_1) [topological_space α] [discrete_topology α] :

topological_space.is_topological_basis {s : set α | ∃ (x : α), s = {x}}

@[protected]

theorem dense_range.separable_space {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space.separable_space α] [topological_space β] {f : α → β} (h : dense_range f) (h' : continuous f) :

topological_space.separable_space β

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 {α : Type u_1} [topological_space α] {s : set α} [topological_space.separable_space ↥s] (hs : dense s) :

∃ (t : set α) (H : t ⊆ s), t.countable ∧ dense t

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.

@[protected, instance]

def separable_space_univ {α : Type u_1} [topological_space α] [topological_space.separable_space α] :

topological_space.separable_space ↥set.univ

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.

@[class]

structure topological_space.first_countable_topology (α : Type u) [t : topological_space α] :

Prop

nhds_generated_countable : ∀ (a : α), (nhds a).is_countably_generated

A first-countable space is one in which every point has a countable neighborhood basis.

Instances of this typeclass

theorem topological_space.first_countable_topology.tendsto_subseq {α : Type u} [t : topological_space α] [topological_space.first_countable_topology α] {u : ℕ → α} {x : α} (hx : map_cluster_pt x filter.at_top u) :

∃ (ψ : ℕ → ℕ), strict_mono ψ ∧ filter.tendsto (u ∘ ψ) filter.at_top (nhds x)

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

@[protected, instance]

def topological_space.prod.first_countable_topology {α : Type u} [t : topological_space α] {β : Type u_1} [topological_space β] [topological_space.first_countable_topology α] [topological_space.first_countable_topology β] :

topological_space.first_countable_topology (α × β)

@[protected, instance]

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

topological_space.first_countable_topology (Π (i : ι), π i)

@[protected, instance]

def topological_space.is_countably_generated_nhds_within {α : Type u} [t : topological_space α] (x : α) [(nhds x).is_countably_generated] (s : set α) :

(nhds_within x s).is_countably_generated

@[class]

structure topological_space.second_countable_topology (α : Type u) [t : topological_space α] :

Prop

is_open_generated_countable : ∃ (b : set (set α)), b.countable ∧ t = topological_space.generate_from b

A second-countable space is one with a countable basis.

Instances of this typeclass

@[protected]

theorem topological_space.is_topological_basis.second_countable_topology {α : Type u} [t : topological_space α] {b : set (set α)} (hb : topological_space.is_topological_basis b) (hc : b.countable) :

topological_space.second_countable_topology α

theorem topological_space.exists_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

∃ (b : set (set α)), b.countable ∧ ∅ ∉ b ∧ topological_space.is_topological_basis b

def topological_space.countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

set (set α)

A countable topological basis of α.

Equations

topological_space.countable_basis α = _.some

Instances for ↥topological_space.countable_basis

topological_space.encodable_countable_basis

theorem topological_space.countable_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

(topological_space.countable_basis α).countable

@[protected, instance]

noncomputable def topological_space.encodable_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

encodable ↥(topological_space.countable_basis α)

Equations

topological_space.encodable_countable_basis α = _.to_encodable

theorem topological_space.empty_nmem_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

∅ ∉ topological_space.countable_basis α

theorem topological_space.is_basis_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

topological_space.is_topological_basis (topological_space.countable_basis α)

theorem topological_space.eq_generate_from_countable_basis (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

t = topological_space.generate_from (topological_space.countable_basis α)

theorem topological_space.is_open_of_mem_countable_basis {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {s : set α} (hs : s ∈ topological_space.countable_basis α) :

theorem topological_space.nonempty_of_mem_countable_basis {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] {s : set α} (hs : s ∈ topological_space.countable_basis α) :

@[protected, instance]

def topological_space.second_countable_topology.to_first_countable_topology (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

topological_space.first_countable_topology α

theorem topological_space.second_countable_topology_induced (α : Type u) (β : Type u_1) [t : topological_space β] [topological_space.second_countable_topology β] (f : α → β) :

topological_space.second_countable_topology α

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

@[protected, instance]

def topological_space.subtype.second_countable_topology (α : Type u) [t : topological_space α] (s : set α) [topological_space.second_countable_topology α] :

topological_space.second_countable_topology ↥s

@[protected, instance]

def topological_space.prod.second_countable_topology (α : Type u) [t : topological_space α] {β : Type u_1} [topological_space β] [topological_space.second_countable_topology α] [topological_space.second_countable_topology β] :

topological_space.second_countable_topology (α × β)

@[protected, instance]

def topological_space.pi.second_countable_topology {ι : Type u_1} {π : ι → Type u_2} [countable ι] [t : Π (a : ι), topological_space (π a)] [∀ (a : ι), topological_space.second_countable_topology (π a)] :

topological_space.second_countable_topology (Π (a : ι), π a)

@[protected, instance]

def topological_space.second_countable_topology.to_separable_space (α : Type u) [t : topological_space α] [topological_space.second_countable_topology α] :

topological_space.separable_space α

theorem topological_space.second_countable_topology_of_countable_cover {α : Type u} [t : topological_space α] {ι : Type u_1} [encodable ι] {U : ι → set α} [∀ (i : ι), topological_space.second_countable_topology ↥(U i)] (Uo : ∀ (i : ι), is_open (U i)) (hc : (⋃ (i : ι), U i) = set.univ) :

topological_space.second_countable_topology α

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.is_open_sUnion_countable {α : Type u} [t : topological_space α] [topological_space.second_countable_topology α] (S : set (set α)) (H : ∀ (s : set α), s ∈ S → is_open s) :

∃ (T : set (set α)), T.countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

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]

def topological_space.sigma.second_countable_topology {ι : Type u_1} {E : ι → Type u_2} [Π (i : ι), topological_space (E i)] [countable ι] [∀ (i : ι), topological_space.second_countable_topology (E i)] :

topological_space.second_countable_topology (Σ (i : ι), E i)

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

theorem topological_space.is_topological_basis.sum {α : Type u} {β : Type u_1} [topological_space α] [topological_space β] {s : set (set α)} (hs : topological_space.is_topological_basis s) {t : set (set β)} (ht : topological_space.is_topological_basis t) :

topological_space.is_topological_basis ((λ (u : set α), sum.inl '' u) '' s ∪ (λ (u : set β), sum.inr '' u) '' t)

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]

def topological_space.sum.second_countable_topology {α : Type u} {β : Type u_1} [topological_space α] [topological_space β] [topological_space.second_countable_topology α] [topological_space.second_countable_topology β] :

topological_space.second_countable_topology (α ⊕ β)

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

theorem topological_space.is_topological_basis.quotient_map {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {π : X → Y} {V : set (set X)} (hV : topological_space.is_topological_basis V) (h' : quotient_map π) (h : is_open_map π) :

topological_space.is_topological_basis (set.image π '' V)

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

theorem topological_space.quotient_map.second_countable_topology {X : Type u_1} [topological_space X] {Y : Type u_2} [topological_space Y] {π : X → Y} [topological_space.second_countable_topology X] (h' : quotient_map π) (h : is_open_map π) :

topological_space.second_countable_topology Y

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

theorem topological_space.is_topological_basis.quotient {X : Type u_1} [topological_space X] {S : setoid X} {V : set (set X)} (hV : topological_space.is_topological_basis V) (h : is_open_map quotient.mk) :

topological_space.is_topological_basis (set.image quotient.mk '' V)

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

theorem topological_space.quotient.second_countable_topology {X : Type u_1} [topological_space X] {S : setoid X} [topological_space.second_countable_topology X] (h : is_open_map quotient.mk) :

topological_space.second_countable_topology (quotient S)

An open quotient of a second countable space is second countable.

@[protected]

theorem inducing.second_countable_topology {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} [topological_space.second_countable_topology β] (hf : inducing f) :

topological_space.second_countable_topology α

@[protected]

theorem embedding.second_countable_topology {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} [topological_space.second_countable_topology β] (hf : embedding f) :

topological_space.second_countable_topology α