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.
• TopologicalSpace.FirstCountableTopology α: A topology in which 𝓝 x is countably generated for every x.
• TopologicalSpace.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 TopologicalSpace.FirstCountableTopology, TopologicalSpace.SeparableSpace, and more.

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

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

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

theorem 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 => ⋂₀ f) '' {f | 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_open_of_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : ∀ (u : Set α), u ∈ s → IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, 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, 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 : α), a ∈ s → ∃ t, 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 => t ∈ b ∧ a ∈ t) fun t => 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, 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 | 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, 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, 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) : ∃ β f, 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 : Set α), 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 : Set α), 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 : Set α), 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 : Set α), 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_1} [TopologicalSpace β] {B : Set (Set α)} (hB : TopologicalSpace.IsTopologicalBasis B) {f : α → β} : IsOpenMap f ↔ ∀ (s : Set α), 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, v ∈ B ∧ Set.Nonempty v ∧ v ⊆ u

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

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

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

theorem TopologicalSpace.isTopologicalBasis_of_cover {α : Type u} [t : TopologicalSpace α] {ι : Sort u_1} {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 {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] {B : Set (Set β)} (hB : TopologicalSpace.IsTopologicalBasis B) (f : α → β) (hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)) : Continuous f

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

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

• exists_countable_dense : ∃ s, Set.Countable s ∧ Dense s

  There exists a countable dense set.

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 TopologicalSpace.SecondCountableTopology α. In this case the latter should be used as a typeclass argument in theorems because Lean can automatically deduce TopologicalSpace.SeparableSpace from TopologicalSpace.SecondCountableTopology but it can't deduce TopologicalSpace.SecondCountableTopology from TopologicalSpace.SeparableSpace.

Porting note: 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.

theorem TopologicalSpace.exists_countable_dense (α : Type u) [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] : ∃ s, 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 (_ : ∃ u, DenseRange u)

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

• @TopologicalSpace.Countable.to_separableSpace = @TopologicalSpace.Countable.to_separableSpace.proof_1

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

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

The product of two separable spaces is a separable space.

Equations

• @TopologicalSpace.instSeparableSpaceProdInstTopologicalSpaceProd = @TopologicalSpace.instSeparableSpaceProdInstTopologicalSpaceProd.proof_1

instance TopologicalSpace.instSeparableSpaceForAllTopologicalSpace {ι : Type u_1} {X : ι → Type u_2} [(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

• @TopologicalSpace.instSeparableSpaceForAllTopologicalSpace = @TopologicalSpace.instSeparableSpaceForAllTopologicalSpace.proof_1

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

Equations

• @TopologicalSpace.instSeparableSpaceQuotInstTopologicalSpaceQuot = @TopologicalSpace.instSeparableSpaceQuotInstTopologicalSpaceQuot.proof_1

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

Equations

• @TopologicalSpace.instSeparableSpaceQuotientInstTopologicalSpaceQuotient = @TopologicalSpace.instSeparableSpaceQuotientInstTopologicalSpaceQuotient.proof_1

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 Set.PairwiseDisjoint.countable_of_isOpen {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_1} {s : ι → Set α} {a : Set ι} (h : Set.PairwiseDisjoint a s) (ha : ∀ (i : ι), i ∈ a → IsOpen (s i)) (h'a : ∀ (i : ι), 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_1} {s : ι → Set α} {a : Set ι} (h : Set.PairwiseDisjoint a s) (ha : ∀ (i : ι), 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.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.union {α : Type u} [t : TopologicalSpace α] {s : Set α} {u : Set α} (hs : TopologicalSpace.IsSeparable s) (hu : TopologicalSpace.IsSeparable u) : TopologicalSpace.IsSeparable (s ∪ u)

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

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

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

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

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_iff {α : Type u} [t : TopologicalSpace α] : TopologicalSpace.IsSeparable Set.univ ↔ TopologicalSpace.SeparableSpace α

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

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

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

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 | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}

theorem isTopologicalBasis_iInf {β : 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 | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = ⋂ (i : ι) (_ : i ∈ F), f i ⁻¹' U i}

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

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

• @separableSpace_univ = @separableSpace_univ.proof_1

theorem exists_countable_dense_bot_top (α : Type u_1) [TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [PartialOrder α] : ∃ s, 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 TopologicalSpace.FirstCountableTopology (α : Type u) [t : TopologicalSpace α] : Prop

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

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

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

theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq {α : Type u} [t : TopologicalSpace α] [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 β] [TopologicalSpace.FirstCountableTopology α] [TopologicalSpace.FirstCountableTopology β] : TopologicalSpace.FirstCountableTopology (α × β)

Equations

• @TopologicalSpace.instFirstCountableTopologyProdInstTopologicalSpaceProd = @TopologicalSpace.instFirstCountableTopologyProdInstTopologicalSpaceProd.proof_1

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

Equations

• @TopologicalSpace.instFirstCountableTopologyForAllTopologicalSpace = @TopologicalSpace.instFirstCountableTopologyForAllTopologicalSpace.proof_1

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

Equations

• @TopologicalSpace.isCountablyGenerated_nhdsWithin = @TopologicalSpace.isCountablyGenerated_nhdsWithin.proof_1

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

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

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

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

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

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

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

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

A countable topological basis of α.

Equations

• TopologicalSpace.countableBasis α = Exists.choose (_ : ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ TopologicalSpace.IsTopologicalBasis b)

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

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

Equations

• TopologicalSpace.encodableCountableBasis α = Set.Countable.toEncodable (_ : Set.Countable (TopologicalSpace.countableBasis α))

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

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

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

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

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

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

Equations

• TopologicalSpace.SecondCountableTopology.to_firstCountableTopology = TopologicalSpace.SecondCountableTopology.to_firstCountableTopology.proof_1

theorem TopologicalSpace.secondCountableTopology_induced (α : Type u) (β : Type u_1) [t : TopologicalSpace β] [TopologicalSpace.SecondCountableTopology β] (f : α → β) : TopologicalSpace.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 α) [TopologicalSpace.SecondCountableTopology α] : TopologicalSpace.SecondCountableTopology ↑s

Equations

• @TopologicalSpace.Subtype.secondCountableTopology = @TopologicalSpace.Subtype.secondCountableTopology.proof_1

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

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

Equations

• @TopologicalSpace.instSecondCountableTopologyProdInstTopologicalSpaceProd = @TopologicalSpace.instSecondCountableTopologyProdInstTopologicalSpaceProd.proof_1

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

Equations

• @TopologicalSpace.instSecondCountableTopologyForAllTopologicalSpace = @TopologicalSpace.instSecondCountableTopologyForAllTopologicalSpace.proof_1

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

Equations

• @TopologicalSpace.SecondCountableTopology.to_separableSpace = @TopologicalSpace.SecondCountableTopology.to_separableSpace.proof_1

theorem TopologicalSpace.secondCountableTopology_of_countable_cover {α : Type u} [t : TopologicalSpace α] {ι : Type u_1} [Encodable ι] {U : ι → Set α} [∀ (i : ι), TopologicalSpace.SecondCountableTopology ↑(U i)] (Uo : ∀ (i : ι), IsOpen (U i)) (hc : ⋃ (i : ι), U i = Set.univ) : TopologicalSpace.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 α] [TopologicalSpace.SecondCountableTopology α] {ι : Type u_1} (s : ι → Set α) (H : ∀ (i : ι), IsOpen (s i)) : ∃ T, Set.Countable T ∧ ⋃ (i : ι) (_ : 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_sUnion_countable {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SecondCountableTopology α] (S : Set (Set α)) (H : ∀ (s : Set α), s ∈ S → IsOpen s) : ∃ T, Set.Countable T ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

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

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

Equations

• @TopologicalSpace.instSecondCountableTopologySigmaInstTopologicalSpaceSigma = @TopologicalSpace.instSecondCountableTopologySigmaInstTopologicalSpaceSigma.proof_1

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 => Sum.inl '' u) '' s ∪ (fun u => 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 β] [TopologicalSpace.SecondCountableTopology α] [TopologicalSpace.SecondCountableTopology β] : TopologicalSpace.SecondCountableTopology (α ⊕ β)

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

Equations

• @TopologicalSpace.instSecondCountableTopologySumInstTopologicalSpaceSum = @TopologicalSpace.instSecondCountableTopologySumInstTopologicalSpaceSum.proof_1

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} [TopologicalSpace.SecondCountableTopology X] (h' : QuotientMap π) (h : IsOpenMap π) : TopologicalSpace.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} [TopologicalSpace.SecondCountableTopology X] (h : IsOpenMap Quotient.mk') : TopologicalSpace.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 : α → β} [TopologicalSpace.SecondCountableTopology β] (hf : Inducing f) : TopologicalSpace.SecondCountableTopology α

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