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

• TopologicalSpace.IsTopologicalBasis s: The topological space t has basis s.
• TopologicalSpace.SeparableSpace α: The topological space t has a countable, dense subset.
• TopologicalSpace.IsSeparable s: The set s is contained in the closure of a countable set.
• FirstCountableTopology α: A topology in which 𝓝 x is countably generated for every x.
• SecondCountableTopology α: A topology which has a topological basis which is countable.

## Main results #

• TopologicalSpace.FirstCountableTopology.tendsto_subseq: In a first-countable space, cluster points are limits of subsequences.
• TopologicalSpace.SecondCountableTopology.isOpen_iUnion_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.
• TopologicalSpace.SecondCountableTopology.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 FirstCountableTopology, TopologicalSpace.SeparableSpace, and more.

structure TopologicalSpace.IsTopologicalBasis {α : Type u} [t : ] (s : Set (Set α)) :

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

• exists_subset_inter : t₁s, t₂s, xt₁ t₂, t₃s, x t₃ t₃ t₁ t₂

For every point x, the set of t ∈ s such that x ∈ t is directed downwards.

• sUnion_eq : ⋃₀ s = Set.univ

The sets from s cover the whole space.

• eq_generateFrom :

The topology is generated by sets from s.

Instances For
theorem TopologicalSpace.IsTopologicalBasis.exists_subset_inter {α : Type u} [t : ] {s : Set (Set α)} (self : ) (t₁ : Set α) :
t₁ st₂s, xt₁ t₂, t₃s, x t₃ t₃ t₁ t₂

For every point x, the set of t ∈ s such that x ∈ t is directed downwards.

theorem TopologicalSpace.IsTopologicalBasis.sUnion_eq {α : Type u} [t : ] {s : Set (Set α)} (self : ) :
⋃₀ s = Set.univ

The sets from s cover the whole space.

theorem TopologicalSpace.IsTopologicalBasis.eq_generateFrom {α : Type u} [t : ] {s : Set (Set α)} (self : ) :

The topology is generated by sets from s.

theorem TopologicalSpace.isTopologicalBasis_of_subbasis {α : Type u} [t : ] {s : Set (Set α)} (hs : ) :
TopologicalSpace.IsTopologicalBasis ((fun (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 TopologicalSpace.isTopologicalBasis_of_subbasis_of_finiteInter {α : Type u} [t : ] {s : Set (Set α)} (hsg : ) (hsi : ) :
theorem TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter {α : Type u} [t : ] {r : Set (Set α)} (hsg : ) (hsi : ∀ ⦃s : Set α⦄, s r∀ ⦃t : Set α⦄, t rs t r) :
theorem TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds {α : Type u} [t : ] {s : Set (Set α)} (h_nhds : ∀ (a : α), (nhds a).HasBasis (fun (t : Set α) => t s a t) id) :
theorem TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds {α : Type u} [t : ] {s : Set (Set α)} (h_open : us, ) (h_nhds : ∀ (a : α) (u : Set α), a uvs, 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 TopologicalSpace.IsTopologicalBasis.mem_nhds_iff {α : Type u} [t : ] {a : α} {s : Set α} {b : Set (Set α)} :
s nhds a tb, 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 TopologicalSpace.IsTopologicalBasis.isOpen_iff {α : Type u} [t : ] {s : Set α} {b : Set (Set α)} :
as, tb, a t t s
theorem TopologicalSpace.IsTopologicalBasis.nhds_hasBasis {α : Type u} [t : ] {b : Set (Set α)} {a : α} :
(nhds a).HasBasis (fun (t : Set α) => t b a t) fun (t : Set α) => t
theorem TopologicalSpace.IsTopologicalBasis.isOpen {α : Type u} [t : ] {s : Set α} {b : Set (Set α)} (hs : s b) :
theorem TopologicalSpace.IsTopologicalBasis.mem_nhds {α : Type u} [t : ] {a : α} {s : Set α} {b : Set (Set α)} (hs : s b) (ha : a s) :
s nhds a
theorem TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open {α : Type u} [t : ] {b : Set (Set α)} {a : α} {u : Set α} (au : a u) (ou : ) :
vb, a v v u
theorem TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' {α : Type u} [t : ] {B : Set (Set α)} {u : Set α} (ou : ) :
u = ⋃₀ {s : Set α | s B s u}

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

theorem TopologicalSpace.IsTopologicalBasis.open_eq_sUnion {α : Type u} [t : ] {B : Set (Set α)} {u : Set α} (ou : ) :
SB, u = ⋃₀ S
theorem TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion {α : Type u} [t : ] {B : Set (Set α)} {u : Set α} :
SB, u = ⋃₀ S
theorem TopologicalSpace.IsTopologicalBasis.open_eq_iUnion {α : Type u} [t : ] {B : Set (Set α)} {u : Set α} (ou : ) :
∃ (β : Type u) (f : βSet α), u = ⋃ (i : β), f i ∀ (i : β), f i B
theorem TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset {α : Type u} [t : ] {B : Set (Set α)} {s : Set α} {t : Set α} (hs : ) (h : UB, U sU t) :
s t
theorem TopologicalSpace.IsTopologicalBasis.eq_of_forall_subset_iff {α : Type u} [t : ] {B : Set (Set α)} {s : Set α} {t : Set α} (hs : ) (ht : ) (h : UB, U s U t) :
s = t
theorem TopologicalSpace.IsTopologicalBasis.mem_closure_iff {α : Type u} [t : ] {b : Set (Set α)} {s : Set α} {a : α} :
a ob, a o(o s).Nonempty

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

theorem TopologicalSpace.IsTopologicalBasis.dense_iff {α : Type u} [t : ] {b : Set (Set α)} {s : Set α} :
ob, o.Nonempty(o s).Nonempty

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

theorem TopologicalSpace.IsTopologicalBasis.isOpenMap_iff {α : Type u} [t : ] {β : Type u_2} [] {B : Set (Set α)} {f : αβ} :
sB, IsOpen (f '' s)
theorem TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset {α : Type u} [t : ] {B : Set (Set α)} {u : Set α} (hu : u.Nonempty) (ou : ) :
vB, v.Nonempty v u
theorem TopologicalSpace.IsTopologicalBasis.inducing {α : Type u} [t : ] {β : Type u_2} [] {f : αβ} {T : Set (Set β)} (hf : ) :
theorem TopologicalSpace.IsTopologicalBasis.induced {β : Type u_1} {α : Type u_2} [s : ] (f : αβ) {T : Set (Set β)} :
theorem TopologicalSpace.IsTopologicalBasis.inf {β : Type u_1} {t₁ : } {t₂ : } {B₁ : Set (Set β)} {B₂ : Set (Set β)} (h₁ : ) (h₂ : ) :
TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x1 x2 : Set β) => x1 x2) B₁ B₂)
theorem TopologicalSpace.IsTopologicalBasis.inf_induced {α : Type u} {β : Type u_1} [t : ] {γ : Type u_2} [s : ] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : ) (h₂ : ) (f₁ : γα) (f₂ : γβ) :
TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x1 : Set α) (x2 : Set β) => f₁ ⁻¹' x1 f₂ ⁻¹' x2) B₁ B₂)
theorem TopologicalSpace.IsTopologicalBasis.prod {α : Type u} [t : ] {β : Type u_2} [] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : ) (h₂ : ) :
TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) B₁ B₂)
theorem TopologicalSpace.isTopologicalBasis_of_cover {α : Type u} [t : ] {ι : Sort u_2} {U : ιSet α} (Uo : ∀ (i : ι), IsOpen (U i)) (Uc : ⋃ (i : ι), U i = Set.univ) {b : (i : ι) → Set (Set (U i))} (hb : ∀ (i : ι), ) :
TopologicalSpace.IsTopologicalBasis (⋃ (i : ι), Set.image Subtype.val '' b i)
theorem TopologicalSpace.IsTopologicalBasis.continuous_iff {α : Type u} [t : ] {β : Type u_2} [] {B : Set (Set β)} {f : αβ} :
sB, IsOpen (f ⁻¹' s)
@[deprecated]
theorem TopologicalSpace.IsTopologicalBasis.continuous {α : Type u} [t : ] {β : Type u_2} [] {B : Set (Set β)} (f : αβ) (hf : sB, IsOpen (f ⁻¹' s)) :
theorem TopologicalSpace.separableSpace_iff (α : Type u) [t : ] :
∃ (s : Set α), s.Countable

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

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

Porting note (#11215): TODO: the previous paragraph describes the state of the art in Lean 3. We can have instance cycles in Lean 4 but we might want to postpone adding them till after the port.

• exists_countable_dense : ∃ (s : Set α), s.Countable

There exists a countable dense set.

Instances
theorem TopologicalSpace.SeparableSpace.exists_countable_dense {α : Type u} [t : ] [self : ] :
∃ (s : Set α), s.Countable

There exists a countable dense set.

theorem TopologicalSpace.exists_countable_dense (α : Type u) [t : ] :
∃ (s : Set α), s.Countable
theorem TopologicalSpace.exists_dense_seq (α : Type u) [t : ] [] :
∃ (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 TopologicalSpace.denseSeq and TopologicalSpace.denseRange_denseSeq.

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

def TopologicalSpace.denseSeq (α : Type u) [t : ] [] :
α

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

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

Equations
Instances For
@[simp]
theorem TopologicalSpace.denseRange_denseSeq (α : Type u) [t : ] [] :

The sequence TopologicalSpace.denseSeq α has dense range.

@[instance 100]
Equations
• =
theorem TopologicalSpace.SeparableSpace.of_denseRange {α : Type u} [t : ] {ι : Type u_2} [] (u : ια) (hu : ) :

If f has a dense range and its domain is countable, then its codomain is a separable space. See also DenseRange.separableSpace.

theorem DenseRange.separableSpace' {α : Type u} [t : ] {ι : Type u_2} [] (u : ια) (hu : ) :

Alias of TopologicalSpace.SeparableSpace.of_denseRange.

If f has a dense range and its domain is countable, then its codomain is a separable space. See also DenseRange.separableSpace.

theorem DenseRange.separableSpace {α : Type u} {β : Type u_1} [t : ] [] {f : αβ} (h : ) (h' : ) :

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 QuotientMap.separableSpace {α : Type u} {β : Type u_1} [t : ] [] {f : αβ} (hf : ) :
instance TopologicalSpace.instSeparableSpaceProd {α : Type u} {β : Type u_1} [t : ] [] :

The product of two separable spaces is a separable space.

Equations
• =
instance TopologicalSpace.instSeparableSpaceForallOfCountable {ι : Type u_2} {X : ιType u_3} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), ] [] :

The product of a countable family of separable spaces is a separable space.

Equations
• =
instance TopologicalSpace.instSeparableSpaceQuot {α : Type u} [t : ] {r : ααProp} :
Equations
• =
instance TopologicalSpace.instSeparableSpaceQuotient {α : Type u} [t : ] {s : } :
Equations
• =

A topological space with discrete topology is separable iff it is countable.

theorem Pairwise.countable_of_isOpen_disjoint {α : Type u} [t : ] {ι : Type u_2} {s : ιSet α} (hd : Pairwise (Disjoint on s)) (ho : ∀ (i : ι), IsOpen (s i)) (hne : ∀ (i : ι), (s i).Nonempty) :

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

theorem Set.PairwiseDisjoint.countable_of_isOpen {α : Type u} [t : ] {ι : Type u_2} {s : ιSet α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ia, IsOpen (s i)) (hne : ia, (s i).Nonempty) :
a.Countable

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

theorem Set.PairwiseDisjoint.countable_of_nonempty_interior {α : Type u} [t : ] {ι : Type u_2} {s : ιSet α} {a : Set ι} (h : a.PairwiseDisjoint s) (ha : ia, (interior (s i)).Nonempty) :
a.Countable

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

def TopologicalSpace.IsSeparable {α : Type u} [t : ] (s : Set α) :

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 TopologicalSpace.SeparableSpace s or TopologicalSpace.IsSeparable (univ : Set s)). In metric spaces, the two definitions are equivalent, see TopologicalSpace.IsSeparable.separableSpace.

Equations
Instances For
theorem TopologicalSpace.IsSeparable.mono {α : Type u} [t : ] {s : Set α} {u : Set α} (hs : ) (hu : u s) :
theorem TopologicalSpace.IsSeparable.iUnion {α : Type u} [t : ] {ι : Sort u_2} [] {s : ιSet α} (hs : ∀ (i : ι), ) :
TopologicalSpace.IsSeparable (⋃ (i : ι), s i)
@[simp]
theorem TopologicalSpace.isSeparable_iUnion {α : Type u} [t : ] {ι : Sort u_2} [] {s : ιSet α} :
TopologicalSpace.IsSeparable (⋃ (i : ι), s i) ∀ (i : ι),
@[simp]
theorem TopologicalSpace.isSeparable_union {α : Type u} [t : ] {s : Set α} {t : Set α} :
theorem TopologicalSpace.IsSeparable.union {α : Type u} [t : ] {s : Set α} {u : Set α} (hs : ) (hu : ) :
@[simp]
theorem TopologicalSpace.isSeparable_closure {α : Type u} [t : ] {s : Set α} :
theorem TopologicalSpace.IsSeparable.closure {α : Type u} [t : ] {s : Set α} :

Alias of the reverse direction of TopologicalSpace.isSeparable_closure.

theorem Set.Countable.isSeparable {α : Type u} [t : ] {s : Set α} (hs : s.Countable) :
theorem Set.Finite.isSeparable {α : Type u} [t : ] {s : Set α} (hs : s.Finite) :
theorem TopologicalSpace.IsSeparable.univ_pi {ι : Type u_2} [] {X : ιType u_3} {s : (i : ι) → Set (X i)} [(i : ι) → TopologicalSpace (X i)] (h : ∀ (i : ι), ) :
theorem TopologicalSpace.isSeparable_pi {ι : Type u_2} [] {α : ιType u_3} {s : (i : ι) → Set (α i)} [(i : ι) → TopologicalSpace (α i)] (h : ∀ (i : ι), ) :
TopologicalSpace.IsSeparable {f : (i : ι) → α i | ∀ (i : ι), f i s i}
theorem TopologicalSpace.IsSeparable.prod {α : Type u} [t : ] {β : Type u_2} [] {s : Set α} {t : Set β} (hs : ) (ht : ) :
theorem TopologicalSpace.IsSeparable.image {α : Type u} [t : ] {β : Type u_2} [] {s : Set α} (hs : ) {f : αβ} (hf : ) :
theorem Dense.isSeparable_iff {α : Type u} [t : ] {s : Set α} (hs : ) :
theorem TopologicalSpace.isSeparable_range {α : Type u} {β : Type u_1} [t : ] [] {f : αβ} (hf : ) :
theorem TopologicalSpace.IsSeparable.of_subtype {α : Type u} [t : ] (s : Set α) :
@[deprecated TopologicalSpace.IsSeparable.of_subtype]

Alias of TopologicalSpace.IsSeparable.of_subtype.

@[deprecated TopologicalSpace.IsSeparable.of_separableSpace]
theorem TopologicalSpace.isSeparable_of_separableSpace {α : Type u} [t : ] (s : Set α) :

Alias of TopologicalSpace.IsSeparable.of_separableSpace.

theorem IsTopologicalBasis.iInf {β : Type u_1} {ι : Type u_2} {t : ι} {T : ιSet (Set β)} (h_basis : ∀ (i : ι), ) :
TopologicalSpace.IsTopologicalBasis {S : Set β | ∃ (U : ιSet β) (F : ), (∀ iF, U i T i) S = iF, U i}
theorem IsTopologicalBasis.iInf_induced {β : Type u_1} {ι : Type u_2} {X : ιType u_3} [t : (i : ι) → TopologicalSpace (X i)] {T : (i : ι) → Set (Set (X i))} (cond : ∀ (i : ι), ) (f : (i : ι) → βX i) :
TopologicalSpace.IsTopologicalBasis {S : Set β | ∃ (U : (i : ι) → Set (X i)) (F : ), (∀ iF, U i T i) S = iF, f i ⁻¹' U i}
theorem isTopologicalBasis_pi {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {T : (i : ι) → Set (Set (X i))} (cond : ∀ (i : ι), ) :
TopologicalSpace.IsTopologicalBasis {S : Set ((i : ι) → X i) | ∃ (U : (i : ι) → Set (X i)) (F : ), (∀ iF, U i T i) S = (↑F).pi U}
theorem isTopologicalBasis_singletons (α : Type u_1) [] [] :
TopologicalSpace.IsTopologicalBasis {s : Set α | ∃ (x : α), s = {x}}
theorem isTopologicalBasis_subtype {α : Type u_1} [] {B : Set (Set α)} (p : αProp) :
theorem isOpenMap_eval {ι : Type u_1} {π : ιType u_2} [(i : ι) → TopologicalSpace (π i)] (i : ι) :
theorem Dense.exists_countable_dense_subset {α : Type u_1} [] {s : Set α} (hs : ) :
ts, t.Countable
theorem Dense.exists_countable_dense_subset_bot_top {α : Type u_1} [] [] {s : Set α} (hs : ) :
ts, t.Countable (∀ (x : α), x sx t) ∀ (x : α), x sx 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.

instance separableSpace_univ {α : Type u_1} [] :
Equations
• =
theorem exists_countable_dense_bot_top (α : Type u_1) [] [] :
∃ (s : Set α), s.Countable (∀ (x : α), x s) ∀ (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 FirstCountableTopology (α : Type u) [t : ] :

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

• nhds_generated_countable : ∀ (a : α), (nhds a).IsCountablyGenerated

The filter 𝓝 a is countably generated for all points a.

Instances
theorem FirstCountableTopology.nhds_generated_countable {α : Type u} [t : ] [self : ] (a : α) :
(nhds a).IsCountablyGenerated

The filter 𝓝 a is countably generated for all points a.

theorem TopologicalSpace.firstCountableTopology_induced (α : Type u_1) (β : Type u_2) [t : ] (f : αβ) :

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

instance TopologicalSpace.Subtype.firstCountableTopology {α : Type u} [t : ] (s : Set α) :
Equations
• =
theorem Inducing.firstCountableTopology {α : Type u} [t : ] {β : Type u_1} [] {f : αβ} (hf : ) :
theorem Embedding.firstCountableTopology {α : Type u} [t : ] {β : Type u_1} [] {f : αβ} (hf : ) :
theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq {α : Type u} [t : ] {u : α} {x : α} (hx : MapClusterPt x Filter.atTop u) :
∃ (ψ : ), Filter.Tendsto (u ψ) Filter.atTop (nhds x)

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

Equations
• =
instance TopologicalSpace.instFirstCountableTopologyForallOfCountable {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), ] :
FirstCountableTopology ((i : ι) → π i)
Equations
• =
instance TopologicalSpace.isCountablyGenerated_nhdsWithin {α : Type u} [t : ] (x : α) [(nhds x).IsCountablyGenerated] (s : Set α) :
(nhdsWithin x s).IsCountablyGenerated
Equations
• =
class SecondCountableTopology (α : Type u) [t : ] :

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

• is_open_generated_countable : ∃ (b : Set (Set α)), b.Countable

There exists a countable set of sets that generates the topology.

Instances
theorem SecondCountableTopology.is_open_generated_countable {α : Type u} [t : ] [self : ] :
∃ (b : Set (Set α)), b.Countable

There exists a countable set of sets that generates the topology.

theorem TopologicalSpace.IsTopologicalBasis.secondCountableTopology {α : Type u} [t : ] {b : Set (Set α)} (hc : b.Countable) :
theorem TopologicalSpace.SecondCountableTopology.mk' {α : Type u_1} {b : Set (Set α)} (hc : b.Countable) :
instance Finite.toSecondCountableTopology {α : Type u} [t : ] [] :
Equations
• =
theorem TopologicalSpace.exists_countable_basis (α : Type u) [t : ] :
∃ (b : Set (Set α)), b.Countable
def TopologicalSpace.countableBasis (α : Type u) [t : ] :
Set (Set α)

A countable topological basis of α.

Equations
• = .choose
Instances For
theorem TopologicalSpace.countable_countableBasis (α : Type u) [t : ] :
.Countable
Equations
• = .toEncodable
theorem TopologicalSpace.isOpen_of_mem_countableBasis {α : Type u} [t : ] {s : Set α} (hs : ) :
theorem TopologicalSpace.nonempty_of_mem_countableBasis {α : Type u} [t : ] {s : Set α} (hs : ) :
s.Nonempty
@[instance 100]
Equations
• =
theorem TopologicalSpace.secondCountableTopology_induced (α : Type u_1) (β : Type u_2) [t : ] (f : αβ) :

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

instance TopologicalSpace.Subtype.secondCountableTopology {α : Type u} [t : ] (s : Set α) :
Equations
• =
theorem TopologicalSpace.secondCountableTopology_iInf {α : Type u_1} {ι : Sort u_2} [] {t : ι} (ht : ∀ (i : ι), ) :
Equations
• =
instance TopologicalSpace.instSecondCountableTopologyForallOfCountable {ι : Type u_1} {π : ιType u_2} [] [(a : ι) → TopologicalSpace (π a)] [∀ (a : ι), ] :
SecondCountableTopology ((a : ι) → π a)
Equations
• =
@[instance 100]
Equations
• =
theorem TopologicalSpace.secondCountableTopology_of_countable_cover {α : Type u} [t : ] {ι : Sort u_1} [] {U : ιSet α} [∀ (i : ι), SecondCountableTopology (U i)] (Uo : ∀ (i : ι), IsOpen (U i)) (hc : ⋃ (i : ι), U i = Set.univ) :

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

theorem TopologicalSpace.isOpen_iUnion_countable {α : Type u} [t : ] {ι : Type u_1} (s : ιSet α) (H : ∀ (i : ι), IsOpen (s i)) :
∃ (T : Set ι), T.Countable iT, 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. In particular, any open covering of α has a countable subcover: α is a Lindelöf space.

theorem TopologicalSpace.isOpen_biUnion_countable {α : Type u} [t : ] {ι : Type u_1} (I : Set ι) (s : ιSet α) (H : iI, IsOpen (s i)) :
TI, T.Countable iT, s i = iI, s i
theorem TopologicalSpace.isOpen_sUnion_countable {α : Type u} [t : ] (S : Set (Set α)) (H : sS, ) :
∃ (T : Set (Set α)), T.Countable T S ⋃₀ T = ⋃₀ S
theorem TopologicalSpace.countable_cover_nhds {α : Type u} [t : ] {f : αSet α} (hf : ∀ (x : α), f x nhds x) :
∃ (s : Set α), s.Countable xs, 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 TopologicalSpace.countable_cover_nhdsWithin {α : Type u} [t : ] {f : αSet α} {s : Set α} (hf : xs, f x ) :
ts, t.Countable s xt, f x
theorem TopologicalSpace.IsTopologicalBasis.sigma {ι : Type u_1} {E : ιType u_2} [(i : ι) → TopologicalSpace (E i)] {s : (i : ι) → Set (Set (E i))} (hs : ∀ (i : ι), ) :
TopologicalSpace.IsTopologicalBasis (⋃ (i : ι), (fun (u : Set (E 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.

instance TopologicalSpace.instSecondCountableTopologySigmaOfCountable {ι : Type u_1} {E : ιType u_2} [(i : ι) → TopologicalSpace (E i)] [] [∀ (i : ι), ] :
SecondCountableTopology ((i : ι) × E i)

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

Equations
• =
theorem TopologicalSpace.IsTopologicalBasis.sum {α : Type u} [t : ] {β : Type u_1} [] {s : Set (Set α)} {t : Set (Set β)} :
TopologicalSpace.IsTopologicalBasis ((fun (u : Set α) => Sum.inl '' u) '' s (fun (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.

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

Equations
• =
theorem TopologicalSpace.IsTopologicalBasis.quotientMap {X : Type u_1} [] {Y : Type u_2} [] {π : XY} {V : Set (Set X)} (h' : ) (h : ) :

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

theorem QuotientMap.secondCountableTopology {X : Type u_1} [] {Y : Type u_2} [] {π : XY} (h' : ) (h : ) :

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

theorem TopologicalSpace.IsTopologicalBasis.quotient {X : Type u_1} [] {S : } {V : Set (Set X)} (h : IsOpenMap Quotient.mk') :

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

theorem TopologicalSpace.Quotient.secondCountableTopology {X : Type u_1} [] {S : } (h : IsOpenMap Quotient.mk') :

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

theorem Inducing.secondCountableTopology {α : Type u_1} {β : Type u_2} [] {f : αβ} [] (hf : ) :
theorem Embedding.secondCountableTopology {α : Type u_1} {β : Type u_2} [] {f : αβ} [] (hf : ) :
theorem Embedding.separableSpace {α : Type u_1} {β : Type u_2} [] [] {f : αβ} (hf : ) :