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 : TopologicalSpace α] (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).

• exists_subset_inter (t₁ : Set α) : t₁ ∈ s → ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ 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 : t = generateFrom s

  The topology is generated by sets from s.

theorem TopologicalSpace.isTopologicalBasis_of_subbasis {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (hs : t = generateFrom s) : 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 : TopologicalSpace α] {s : Set (Set α)} (hsg : t = generateFrom s) (hsi : FiniteInter s) : IsTopologicalBasis s

theorem TopologicalSpace.isTopologicalBasis_of_subbasis_of_inter {α : Type u} [t : TopologicalSpace α] {r : Set (Set α)} (hsg : t = generateFrom r) (hsi : ∀ ⦃s : Set α⦄, s ∈ r → ∀ ⦃t : Set α⦄, t ∈ r → s ∩ t ∈ r) : IsTopologicalBasis (insert Set.univ r)

theorem TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_nhds : ∀ (a : α), (nhds a).HasBasis (fun (t : Set α) => t ∈ s ∧ a ∈ t) id) : IsTopologicalBasis s

theorem TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : ∀ u ∈ s, IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) : IsTopologicalBasis 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 TopologicalSpace.IsTopologicalBasis.mem_nhds_iff {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : s ∈ nhds a ↔ ∃ 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 TopologicalSpace.IsTopologicalBasis.isOpen_iff {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) : IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

theorem TopologicalSpace.IsTopologicalBasis.of_isOpen_of_subset {α : Type u} [t : TopologicalSpace α] {s s' : Set (Set α)} (h_open : ∀ u ∈ s', IsOpen u) (hs : IsTopologicalBasis s) (hss' : s ⊆ s') : IsTopologicalBasis s'

theorem TopologicalSpace.IsTopologicalBasis.nhds_hasBasis {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} : (nhds a).HasBasis (fun (t : Set α) => t ∈ b ∧ a ∈ t) fun (t : Set α) => t

theorem TopologicalSpace.IsTopologicalBasis.isOpen {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s

theorem TopologicalSpace.IsTopologicalBasis.insert_empty {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (insert ∅ s)

theorem TopologicalSpace.IsTopologicalBasis.diff_empty {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h : IsTopologicalBasis s) : IsTopologicalBasis (s \ {∅})

theorem TopologicalSpace.IsTopologicalBasis.mem_nhds {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)} (hb : IsTopologicalBasis b) (hs : s ∈ b) (ha : a ∈ s) : s ∈ nhds a

theorem TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} {u : Set α} (au : a ∈ u) (ou : IsOpen u) : ∃ v ∈ b, a ∈ v ∧ v ⊆ u

theorem TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : 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 : TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ S ⊆ B, u = ⋃₀ S

theorem TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S

theorem TopologicalSpace.IsTopologicalBasis.open_eq_iUnion {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hB : IsTopologicalBasis B) {u : Set α} (ou : IsOpen u) : ∃ (β : Type u) (f : β → Set α), u = ⋃ (i : β), f i ∧ ∀ (i : β), f i ∈ B

theorem TopologicalSpace.IsTopologicalBasis.isOpen_induction {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {P : Set α → Prop} (hB : IsTopologicalBasis B) (basis : ∀ b ∈ B, P b) (sUnion : ∀ (S : Set (Set α)), (∀ s ∈ S, P s) → P (⋃₀ S)) {s : Set α} (hs : IsOpen s) : P s

theorem TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t✝ : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t✝) : s ⊆ t✝

theorem TopologicalSpace.IsTopologicalBasis.eq_of_forall_subset_iff {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s t✝ : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (ht : IsOpen t✝) (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t✝) : s = t✝

theorem TopologicalSpace.IsTopologicalBasis.mem_closure_iff {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} {a : α} : a ∈ closure s ↔ ∀ 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 TopologicalSpace.IsTopologicalBasis.dense_iff {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α} : Dense s ↔ ∀ o ∈ b, 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 : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {B : Set (Set α)} (hB : IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)

theorem TopologicalSpace.IsTopologicalBasis.exists_nonempty_subset {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} (hb : IsTopologicalBasis B) {u : Set α} (hu : u.Nonempty) (ou : IsOpen u) : ∃ v ∈ B, v.Nonempty ∧ v ⊆ u

theorem TopologicalSpace.isTopologicalBasis_opens {α : Type u} [t : TopologicalSpace α] : IsTopologicalBasis {U : Set α | IsOpen U}

theorem TopologicalSpace.IsTopologicalBasis.isInducing {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {f : α → β} {T : Set (Set β)} (hf : Topology.IsInducing f) (h : IsTopologicalBasis T) : IsTopologicalBasis (Set.preimage f '' T)

theorem TopologicalSpace.IsTopologicalBasis.induced {β : Type u_1} {α : Type u_2} [s : TopologicalSpace β] (f : α → β) {T : Set (Set β)} (h : IsTopologicalBasis T) : IsTopologicalBasis (Set.preimage f '' T)

theorem TopologicalSpace.IsTopologicalBasis.inf {β : Type u_1} {t₁ t₂ : TopologicalSpace β} {B₁ B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) : IsTopologicalBasis (Set.image2 (fun (x1 x2 : Set β) => x1 ∩ x2) B₁ B₂)

theorem TopologicalSpace.IsTopologicalBasis.inf_induced {α : Type u} {β : Type u_1} [t : TopologicalSpace α] {γ : Type u_2} [s : TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) (f₁ : γ → α) (f₂ : γ → β) : IsTopologicalBasis (Set.image2 (fun (x1 : Set α) (x2 : Set β) => f₁ ⁻¹' x1 ∩ f₂ ⁻¹' x2) B₁ B₂)

theorem TopologicalSpace.IsTopologicalBasis.prod {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁) (h₂ : IsTopologicalBasis B₂) : IsTopologicalBasis (Set.image2 (fun (x1 : Set α) (x2 : Set β) => x1 ×ˢ x2) B₁ B₂)

theorem TopologicalSpace.isTopologicalBasis_of_cover {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} {U : ι → Set α} (Uo : ∀ (i : ι), IsOpen (U i)) (Uc : ⋃ (i : ι), U i = Set.univ) {b : (i : ι) → Set (Set ↑(U i))} (hb : ∀ (i : ι), IsTopologicalBasis (b i)) : IsTopologicalBasis (⋃ (i : ι), Set.image Subtype.val '' b i)

theorem TopologicalSpace.IsTopologicalBasis.continuous_iff {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {B : Set (Set β)} (hB : IsTopologicalBasis B) {f : α → β} : Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

@[simp]

theorem TopologicalSpace.isTopologicalBasis_empty {α : Type u} [t : TopologicalSpace α] : IsTopologicalBasis ∅ ↔ IsEmpty α

class TopologicalSpace.SeparableSpace (α : Type u) [t : TopologicalSpace α] : Prop

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 using TopologicalSpace.SecondCountableTopology.to_separableSpace, but deducing SecondCountableTopology from TopologicalSpace.SeparableSpace requires more assumptions.

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

  There exists a countable dense set.

theorem TopologicalSpace.separableSpace_iff (α : Type u) [t : TopologicalSpace α] : SeparableSpace α ↔ ∃ (s : Set α), s.Countable ∧ Dense s

theorem TopologicalSpace.exists_countable_dense (α : Type u) [t : TopologicalSpace α] [SeparableSpace α] : ∃ (s : Set α), s.Countable ∧ Dense s

theorem TopologicalSpace.exists_dense_seq (α : Type u) [t : TopologicalSpace α] [SeparableSpace α] [Nonempty α] : ∃ (u : ℕ → α), DenseRange 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 : TopologicalSpace α] [SeparableSpace α] [Nonempty α] : ℕ → α

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

• TopologicalSpace.denseSeq α = Classical.choose ⋯

@[simp]

theorem TopologicalSpace.denseRange_denseSeq (α : Type u) [t : TopologicalSpace α] [SeparableSpace α] [Nonempty α] : DenseRange (denseSeq α)

The sequence TopologicalSpace.denseSeq α has dense range.

@[instance 100]

instance TopologicalSpace.Countable.to_separableSpace {α : Type u} [t : TopologicalSpace α] [Countable α] : SeparableSpace α

theorem TopologicalSpace.SeparableSpace.of_denseRange {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [Countable ι] (u : ι → α) (hu : DenseRange u) : SeparableSpace α

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 : TopologicalSpace α] {ι : Type u_2} [Countable ι] (u : ι → α) (hu : DenseRange u) : TopologicalSpace.SeparableSpace α

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 : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [TopologicalSpace β] {f : α → β} (h : DenseRange f) (h' : Continuous f) : TopologicalSpace.SeparableSpace β

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 Topology.IsQuotientMap.separableSpace {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [TopologicalSpace β] {f : α → β} (hf : IsQuotientMap f) : TopologicalSpace.SeparableSpace β

instance TopologicalSpace.instSeparableSpaceProd {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] [SeparableSpace α] [SeparableSpace β] : SeparableSpace (α × β)

The product of two separable spaces is a separable space.

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

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

instance TopologicalSpace.instSeparableSpaceQuot {α : Type u} [t : TopologicalSpace α] [SeparableSpace α] {r : α → α → Prop} : SeparableSpace (Quot r)

instance TopologicalSpace.instSeparableSpaceQuotient {α : Type u} [t : TopologicalSpace α] [SeparableSpace α] {s : Setoid α} : SeparableSpace (Quotient s)

theorem TopologicalSpace.separableSpace_iff_countable {α : Type u} [t : TopologicalSpace α] [DiscreteTopology α] : SeparableSpace α ↔ Countable α

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

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

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

theorem Set.PairwiseDisjoint.countable_of_isOpen {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ho : ∀ i ∈ a, IsOpen (s i)) (hne : ∀ i ∈ a, (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 : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} {a : Set ι} (h : a.PairwiseDisjoint s) (ha : ∀ i ∈ a, (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 : TopologicalSpace α] (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 TopologicalSpace.SeparableSpace s or TopologicalSpace.IsSeparable (univ : Set s)). In metric spaces, the two definitions are equivalent, see TopologicalSpace.IsSeparable.separableSpace.

Equations

• TopologicalSpace.IsSeparable s = ∃ (c : Set α), c.Countable ∧ s ⊆ closure c

theorem TopologicalSpace.IsSeparable.mono {α : Type u} [t : TopologicalSpace α] {s u : Set α} (hs : IsSeparable s) (hu : u ⊆ s) : IsSeparable u

theorem TopologicalSpace.IsSeparable.iUnion {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} [Countable ι] {s : ι → Set α} (hs : ∀ (i : ι), IsSeparable (s i)) : IsSeparable (⋃ (i : ι), s i)

@[simp]

theorem TopologicalSpace.isSeparable_iUnion {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} [Countable ι] {s : ι → Set α} : IsSeparable (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsSeparable (s i)

@[simp]

theorem TopologicalSpace.isSeparable_union {α : Type u} [t : TopologicalSpace α] {s t✝ : Set α} : IsSeparable (s ∪ t✝) ↔ IsSeparable s ∧ IsSeparable t✝

theorem TopologicalSpace.IsSeparable.union {α : Type u} [t : TopologicalSpace α] {s u : Set α} (hs : IsSeparable s) (hu : IsSeparable u) : IsSeparable (s ∪ u)

@[simp]

theorem TopologicalSpace.isSeparable_closure {α : Type u} [t : TopologicalSpace α] {s : Set α} : IsSeparable (closure s) ↔ IsSeparable s

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

Alias of the reverse direction of TopologicalSpace.isSeparable_closure.

theorem Set.Countable.isSeparable {α : Type u} [t : TopologicalSpace α] {s : Set α} (hs : s.Countable) : TopologicalSpace.IsSeparable s

theorem Set.Finite.isSeparable {α : Type u} [t : TopologicalSpace α] {s : Set α} (hs : s.Finite) : TopologicalSpace.IsSeparable s

theorem TopologicalSpace.IsSeparable.univ_pi {ι : Type u_2} [Countable ι] {X : ι → Type u_3} {s : (i : ι) → Set (X i)} [(i : ι) → TopologicalSpace (X i)] (h : ∀ (i : ι), IsSeparable (s i)) : IsSeparable (Set.univ.pi s)

theorem TopologicalSpace.isSeparable_pi {ι : Type u_2} [Countable ι] {α : ι → Type u_3} {s : (i : ι) → Set (α i)} [(i : ι) → TopologicalSpace (α i)] (h : ∀ (i : ι), IsSeparable (s i)) : IsSeparable {f : (i : ι) → α i | ∀ (i : ι), f i ∈ s i}

theorem TopologicalSpace.IsSeparable.prod {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {s : Set α} {t✝ : Set β} (hs : IsSeparable s) (ht : IsSeparable t✝) : IsSeparable (s ×ˢ t✝)

theorem TopologicalSpace.IsSeparable.image {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {s : Set α} (hs : IsSeparable s) {f : α → β} (hf : Continuous f) : IsSeparable (f '' s)

theorem Dense.isSeparable_iff {α : Type u} [t : TopologicalSpace α] {s : Set α} (hs : Dense s) : TopologicalSpace.IsSeparable s ↔ TopologicalSpace.SeparableSpace α

theorem TopologicalSpace.isSeparable_univ_iff {α : Type u} [t : TopologicalSpace α] : IsSeparable Set.univ ↔ SeparableSpace α

theorem TopologicalSpace.isSeparable_range {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace β] [SeparableSpace α] {f : α → β} (hf : Continuous f) : IsSeparable (Set.range f)

theorem TopologicalSpace.IsSeparable.of_subtype {α : Type u} [t : TopologicalSpace α] (s : Set α) [SeparableSpace ↑s] : IsSeparable s

theorem TopologicalSpace.IsSeparable.of_separableSpace {α : Type u} [t : TopologicalSpace α] [h : SeparableSpace α] (s : Set α) : IsSeparable s

theorem IsTopologicalBasis.iInf {β : Type u_1} {ι : Type u_2} {t : ι → TopologicalSpace β} {T : ι → Set (Set β)} (h_basis : ∀ (i : ι), TopologicalSpace.IsTopologicalBasis (T i)) : TopologicalSpace.IsTopologicalBasis {S : Set β | ∃ (U : ι → Set β) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, 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 : ι), TopologicalSpace.IsTopologicalBasis (T i)) (f : (i : ι) → β → X i) : TopologicalSpace.IsTopologicalBasis {S : Set β | ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, 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 (T i)) : TopologicalSpace.IsTopologicalBasis {S : Set ((i : ι) → X i) | ∃ (U : (i : ι) → Set (X i)) (F : Finset ι), (∀ i ∈ F, U i ∈ T i) ∧ S = (↑F).pi U}

theorem isTopologicalBasis_singletons (α : Type u_1) [TopologicalSpace α] [DiscreteTopology α] : TopologicalSpace.IsTopologicalBasis {s : Set α | ∃ (x : α), s = {x}}

theorem isTopologicalBasis_subtype {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) : TopologicalSpace.IsTopologicalBasis (Set.preimage Subtype.val '' B)

theorem isOpenMap_eval {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] (i : ι) : IsOpenMap (Function.eval i)

theorem Dense.exists_countable_dense_subset {α : Type u_1} [TopologicalSpace α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t

theorem Dense.exists_countable_dense_subset_bot_top {α : Type u_1} [TopologicalSpace α] [PartialOrder α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop 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.

instance separableSpace_univ {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] : TopologicalSpace.SeparableSpace ↑Set.univ

theorem exists_countable_dense_bot_top (α : Type u_1) [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [PartialOrder α] : ∃ (s : Set α), s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop 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 : TopologicalSpace α] : Prop

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.

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

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

instance TopologicalSpace.Subtype.firstCountableTopology {α : Type u} [t : TopologicalSpace α] (s : Set α) [FirstCountableTopology α] : FirstCountableTopology ↑s

theorem Topology.IsInducing.firstCountableTopology {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsInducing f) : FirstCountableTopology α

theorem Topology.IsEmbedding.firstCountableTopology {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : IsEmbedding f) : FirstCountableTopology α

theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {u : ℕ → α} {x : α} (hx : MapClusterPt x Filter.atTop u) : ∃ (ψ : ℕ → ℕ), StrictMono ψ ∧ 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.

instance TopologicalSpace.instFirstCountableTopologyProd {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] : FirstCountableTopology (α × β)

instance TopologicalSpace.instFirstCountableTopologyForallOfCountable {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), FirstCountableTopology (X i)] : FirstCountableTopology ((i : ι) → X i)

instance TopologicalSpace.isCountablyGenerated_nhdsWithin {α : Type u} [t : TopologicalSpace α] (x : α) [(nhds x).IsCountablyGenerated] (s : Set α) : (nhdsWithin x s).IsCountablyGenerated

class SecondCountableTopology (α : Type u) [t : TopologicalSpace α] : Prop

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

• is_open_generated_countable : ∃ (b : Set (Set α)), b.Countable ∧ t = TopologicalSpace.generateFrom b

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

theorem TopologicalSpace.IsTopologicalBasis.secondCountableTopology {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : IsTopologicalBasis b) (hc : b.Countable) : SecondCountableTopology α

theorem TopologicalSpace.SecondCountableTopology.mk' {α : Type u_1} {b : Set (Set α)} (hc : b.Countable) : SecondCountableTopology α

instance Finite.toSecondCountableTopology {α : Type u} [t : TopologicalSpace α] [Finite α] : SecondCountableTopology α

theorem TopologicalSpace.exists_countable_basis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b

def TopologicalSpace.countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : Set (Set α)

A countable topological basis of α.

Equations

• TopologicalSpace.countableBasis α = ⋯.choose

theorem TopologicalSpace.countable_countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : (countableBasis α).Countable

instance TopologicalSpace.encodableCountableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : Encodable ↑(countableBasis α)

Equations

• TopologicalSpace.encodableCountableBasis α = ⋯.toEncodable

theorem TopologicalSpace.empty_notMem_countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∅ ∉ countableBasis α

@[deprecated TopologicalSpace.empty_notMem_countableBasis (since := "2025-05-24")]

theorem TopologicalSpace.empty_nmem_countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : ∅ ∉ countableBasis α

Alias of TopologicalSpace.empty_notMem_countableBasis.

theorem TopologicalSpace.isBasis_countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : IsTopologicalBasis (countableBasis α)

theorem TopologicalSpace.eq_generateFrom_countableBasis (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : t = generateFrom (countableBasis α)

theorem TopologicalSpace.isOpen_of_mem_countableBasis {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {s : Set α} (hs : s ∈ countableBasis α) : IsOpen s

theorem TopologicalSpace.nonempty_of_mem_countableBasis {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {s : Set α} (hs : s ∈ countableBasis α) : s.Nonempty

@[instance 100]

instance TopologicalSpace.SecondCountableTopology.to_firstCountableTopology (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α] : FirstCountableTopology α

@[instance 100]

instance TopologicalSpace.instSecondCountableTopologyOfCountableOfFirstCountableTopology (α : Type u) [t : TopologicalSpace α] [Countable α] [FirstCountableTopology α] : SecondCountableTopology α

theorem TopologicalSpace.secondCountableTopology_induced (α : Type u_1) (β : Type u_2) [t : TopologicalSpace β] [SecondCountableTopology β] (f : α → β) : SecondCountableTopology α

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

instance TopologicalSpace.Subtype.secondCountableTopology {α : Type u} [t : TopologicalSpace α] (s : Set α) [SecondCountableTopology α] : SecondCountableTopology ↑s

theorem TopologicalSpace.secondCountableTopology_iInf {α : Type u_1} {ι : Sort u_2} [Countable ι] {t : ι → TopologicalSpace α} (ht : ∀ (i : ι), SecondCountableTopology α) : SecondCountableTopology α

instance TopologicalSpace.instSecondCountableTopologyProd {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] : SecondCountableTopology (α × β)

instance TopologicalSpace.instSecondCountableTopologyForallOfCountable {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [(a : ι) → TopologicalSpace (X a)] [∀ (a : ι), SecondCountableTopology (X a)] : SecondCountableTopology ((a : ι) → X a)

@[instance 100]

instance TopologicalSpace.SecondCountableTopology.to_separableSpace {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] : SeparableSpace α

theorem TopologicalSpace.secondCountableTopology_of_countable_cover {α : Type u} [t : TopologicalSpace α] {ι : Sort u_1} [Countable ι] {U : ι → Set α} [∀ (i : ι), SecondCountableTopology ↑(U i)] (Uo : ∀ (i : ι), IsOpen (U i)) (hc : ⋃ (i : ι), U i = Set.univ) : SecondCountableTopology α

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

theorem TopologicalSpace.isOpen_biUnion_countable {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {ι : Type u_1} (I : Set ι) (s : ι → Set α) (H : ∀ i ∈ I, IsOpen (s i)) : ∃ T ⊆ I, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i ∈ I, s i

theorem TopologicalSpace.isOpen_sUnion_countable {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] (S : Set (Set α)) (H : ∀ s ∈ S, IsOpen s) : ∃ (T : Set (Set α)), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

theorem TopologicalSpace.countable_cover_nhds {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α} (hf : ∀ (x : α), f x ∈ nhds x) : ∃ (s : Set α), s.Countable ∧ ⋃ 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 TopologicalSpace.countable_cover_nhdsWithin {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α} {s : Set α} (hf : ∀ x ∈ s, f x ∈ nhdsWithin x s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

theorem TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : IsTopologicalBasis t✝) {u : Set α} (hu : IsOpen u) : ∃ s ⊆ t✝, s.Countable ∧ u = ⋃ a ∈ s, a

In a second countable topological space, any open set is a countable union of elements in a given topological basis.

theorem TopologicalSpace.IsTopologicalBasis.exists_countable {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {t✝ : Set (Set α)} (ht : IsTopologicalBasis t✝) : ∃ s ⊆ t✝, s.Countable ∧ IsTopologicalBasis s

In a second countable topological space, any topological basis contains a countable subset which is also a topological basis.

theorem TopologicalSpace.exists_countable_of_generateFrom {α : Type u_1} [ts : TopologicalSpace α] [SecondCountableTopology α] {t : Set (Set α)} (ht : ts = generateFrom t) : ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

In a second countable topological space, any family generating the topology admits a countable generating subfamily.

theorem TopologicalSpace.IsTopologicalBasis.sigma {ι : Type u_1} {E : ι → Type u_2} [(i : ι) → TopologicalSpace (E i)] {s : (i : ι) → Set (Set (E i))} (hs : ∀ (i : ι), IsTopologicalBasis (s i)) : IsTopologicalBasis (⋃ (i : ι), (fun (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.

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

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

theorem TopologicalSpace.IsTopologicalBasis.sum {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] {s : Set (Set α)} (hs : IsTopologicalBasis s) {t✝ : Set (Set β)} (ht : IsTopologicalBasis t✝) : 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.

instance TopologicalSpace.instSecondCountableTopologySum {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [SecondCountableTopology α] [SecondCountableTopology β] : SecondCountableTopology (α ⊕ β)

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

theorem TopologicalSpace.IsTopologicalBasis.isQuotientMap {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {π : X → Y} {V : Set (Set X)} (hV : IsTopologicalBasis V) (h' : Topology.IsQuotientMap π) (h : IsOpenMap π) : IsTopologicalBasis (Set.image π '' V)

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

theorem Topology.IsQuotientMap.secondCountableTopology {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {π : X → Y} [SecondCountableTopology X] (h' : IsQuotientMap π) (h : IsOpenMap π) : SecondCountableTopology Y

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

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

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

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

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

theorem Topology.IsInducing.secondCountableTopology {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} [TopologicalSpace β] [SecondCountableTopology β] (hf : IsInducing f) : SecondCountableTopology α

theorem Topology.IsEmbedding.secondCountableTopology {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} [TopologicalSpace β] [SecondCountableTopology β] (hf : IsEmbedding f) : SecondCountableTopology α

theorem Topology.IsEmbedding.separableSpace {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] {f : α → β} (hf : IsEmbedding f) : TopologicalSpace.SeparableSpace α