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₁ ∈ 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 = TopologicalSpace.generateFrom s

  The topology is generated by sets from s.

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

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

theorem TopologicalSpace.isTopologicalBasis_of_subbasis {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (hs : t = TopologicalSpace.generateFrom s) : TopologicalSpace.IsTopologicalBasis ((fun (f : Set (Set α)) => ⋂₀ f) '' {f : Set (Set α) | Set.Finite f ∧ 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_hasBasis_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_nhds : ∀ (a : α), Filter.HasBasis (nhds a) (fun (t : Set α) => t ∈ s ∧ a ∈ t) id) : TopologicalSpace.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) : TopologicalSpace.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 : TopologicalSpace.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 : TopologicalSpace.IsTopologicalBasis b) : IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

theorem TopologicalSpace.IsTopologicalBasis.nhds_hasBasis {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)} (hb : TopologicalSpace.IsTopologicalBasis b) {a : α} : Filter.HasBasis (nhds a) (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 : TopologicalSpace.IsTopologicalBasis b) (hs : s ∈ b) : IsOpen s

theorem TopologicalSpace.IsTopologicalBasis.mem_nhds {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)} (hb : TopologicalSpace.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 : TopologicalSpace.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 : TopologicalSpace.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 : TopologicalSpace.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 : TopologicalSpace.IsTopologicalBasis B) {u : Set α} : IsOpen u ↔ ∃ S ⊆ B, u = ⋃₀ S

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

theorem TopologicalSpace.IsTopologicalBasis.subset_of_forall_subset {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s : Set α} {t : Set α} (hB : TopologicalSpace.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 : Set α} {t : Set α} (hB : TopologicalSpace.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 : TopologicalSpace.IsTopologicalBasis b) {s : Set α} {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → Set.Nonempty (o ∩ s)

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 : TopologicalSpace.IsTopologicalBasis b) {s : Set α} : Dense s ↔ ∀ o ∈ b, Set.Nonempty o → Set.Nonempty (o ∩ s)

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 : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ s ∈ B, IsOpen (f '' s)

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

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

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

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

theorem TopologicalSpace.IsTopologicalBasis.inf {β : Type u_1} {t₁ : TopologicalSpace β} {t₂ : TopologicalSpace β} {B₁ : Set (Set β)} {B₂ : Set (Set β)} (h₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x x_1 : Set β) => x ∩ x_1) 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₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) (f₁ : γ → α) (f₂ : γ → β) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x : Set α) (x_1 : Set β) => f₁ ⁻¹' x ∩ f₂ ⁻¹' x_1) B₁ B₂)

theorem TopologicalSpace.IsTopologicalBasis.prod {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : TopologicalSpace.IsTopologicalBasis B₁) (h₂ : TopologicalSpace.IsTopologicalBasis B₂) : TopologicalSpace.IsTopologicalBasis (Set.image2 (fun (x : Set α) (x_1 : Set β) => x ×ˢ x_1) 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 : ι), TopologicalSpace.IsTopologicalBasis (b i)) : TopologicalSpace.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 : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)

@[deprecated]

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

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

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 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 α), Set.Countable s ∧ Dense s

  There exists a countable dense set.

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

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

The sequence TopologicalSpace.denseSeq α has dense range.

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

Equations

• ⋯ = ⋯

theorem TopologicalSpace.SeparableSpace.of_denseRange {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [Countable ι] (u : ι → α) (hu : DenseRange u) : TopologicalSpace.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 QuotientMap.separableSpace {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [TopologicalSpace β] {f : α → β} (hf : QuotientMap f) : TopologicalSpace.SeparableSpace β

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

The product of two separable spaces is a separable space.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem TopologicalSpace.separableSpace_iff_countable {α : Type u} [t : TopologicalSpace α] [DiscreteTopology α] : TopologicalSpace.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 (Disjoint on s)) (ho : ∀ (i : ι), IsOpen (s i)) (hne : ∀ (i : ι), Set.Nonempty (s i)) : 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 : Set.PairwiseDisjoint a s) (ho : ∀ i ∈ a, IsOpen (s i)) (hne : ∀ i ∈ a, Set.Nonempty (s i)) : Set.Countable a

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 : Set.PairwiseDisjoint a s) (ha : ∀ i ∈ a, Set.Nonempty (interior (s i))) : Set.Countable a

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 α), Set.Countable c ∧ s ⊆ closure c

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

Alias of the reverse direction of TopologicalSpace.isSeparable_closure.

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

theorem Set.Finite.isSeparable {α : Type u} [t : TopologicalSpace α] {s : Set α} (hs : Set.Finite s) : 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 : ι), TopologicalSpace.IsSeparable (s i)) : TopologicalSpace.IsSeparable (Set.pi Set.univ s)

theorem TopologicalSpace.isSeparable_pi {ι : Type u_2} [Countable ι] {α : ι → Type u_3} {s : (i : ι) → Set (α i)} [(i : ι) → TopologicalSpace (α i)] (h : ∀ (i : ι), TopologicalSpace.IsSeparable (s i)) : TopologicalSpace.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 : TopologicalSpace.IsSeparable s) (ht : TopologicalSpace.IsSeparable t) : TopologicalSpace.IsSeparable (s ×ˢ t)

theorem TopologicalSpace.IsSeparable.image {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {s : Set α} (hs : TopologicalSpace.IsSeparable s) {f : α → β} (hf : Continuous f) : TopologicalSpace.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 α] : TopologicalSpace.IsSeparable Set.univ ↔ TopologicalSpace.SeparableSpace α

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

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

@[deprecated TopologicalSpace.IsSeparable.of_subtype]

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

Alias of TopologicalSpace.IsSeparable.of_subtype.

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

@[deprecated TopologicalSpace.IsSeparable.of_separableSpace]

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

Alias of TopologicalSpace.IsSeparable.of_separableSpace.

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 = Set.pi (↑F) 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 Dense.exists_countable_dense_subset {α : Type u_1} [TopologicalSpace α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s] (hs : Dense s) : ∃ t ⊆ s, Set.Countable t ∧ 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, Set.Countable t ∧ 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

Equations

• ⋯ = ⋯

theorem exists_countable_dense_bot_top (α : Type u_1) [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [PartialOrder α] : ∃ (s : Set α), Set.Countable s ∧ 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 : α), Filter.IsCountablyGenerated (nhds a)

  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

Equations

• ⋯ = ⋯

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

theorem Embedding.firstCountableTopology {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [FirstCountableTopology β] {f : α → β} (hf : Embedding 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.instFirstCountableTopologyProdInstTopologicalSpaceProd {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] [FirstCountableTopology α] [FirstCountableTopology β] : FirstCountableTopology (α × β)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

• is_open_generated_countable : ∃ (b : Set (Set α)), Set.Countable b ∧ 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 : TopologicalSpace.IsTopologicalBasis b) (hc : Set.Countable b) : SecondCountableTopology α

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

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

Equations

• ⋯ = ⋯

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

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

A countable topological basis of α.

Equations

• TopologicalSpace.countableBasis α = Exists.choose ⋯

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

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

Equations

• TopologicalSpace.encodableCountableBasis α = Set.Countable.toEncodable ⋯

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

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

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

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

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

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

Equations

• ⋯ = ⋯

theorem TopologicalSpace.secondCountableTopology_induced (α : Type u) (β : Type u_1) [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

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 ι), Set.Countable T ∧ ⋃ 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, Set.Countable T ∧ ⋃ 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 α)), Set.Countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ⋯ = ⋯

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

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

theorem QuotientMap.secondCountableTopology {X : Type u_1} [TopologicalSpace X] {Y : Type u_2} [TopologicalSpace Y] {π : X → Y} [SecondCountableTopology X] (h' : QuotientMap π) (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 : TopologicalSpace.IsTopologicalBasis V) (h : IsOpenMap Quotient.mk') : TopologicalSpace.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 Inducing.secondCountableTopology {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} [SecondCountableTopology β] (hf : Inducing f) : SecondCountableTopology α

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