Documentation

Mathlib.Topology.Bases

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 #

Main results #

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

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

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

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

  • sUnion_eq : ⋃₀ s = Set.univ

    The sets from s cover the whole space.

  • eq_generateFrom : t = TopologicalSpace.generateFrom s

    The topology is generated by sets from s.

Instances For

    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) :
    theorem TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : us, IsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a uIsOpen u∃ v ∈ s, a v v u) :

    If a family of open sets s is such that every open neighbourhood contains some member of s, then s is a topological basis.

    theorem TopologicalSpace.IsTopologicalBasis.mem_nhds_iff {α : Type u} [t : 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 as, ∃ 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.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_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 : UB, U sU 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 : UB, 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 ob, a oSet.Nonempty (o s)

    A point a is in the closure of s iff all basis sets containing a intersect 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 sB, IsOpen (f '' s)
    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 sB, 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 : sB, IsOpen (f ⁻¹' s)) :

    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.

    Instances

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

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

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

      Equations
      Instances For

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

        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.

        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.

        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 ι] :

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

        Equations
        • =

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

        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 : ia, IsOpen (s i)) (hne : ia, Set.Nonempty (s i)) :

        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 : ia, Set.Nonempty (interior (s i))) :

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

        A set s in a topological space is separable if it is contained in the closure of a countable set c. Beware that this definition does not require that c is contained in s (to express the latter, use TopologicalSpace.SeparableSpace s or TopologicalSpace.IsSeparable (univ : Set s)). In metric spaces, the two definitions are equivalent, see TopologicalSpace.IsSeparable.separableSpace.

        Equations
        Instances For
          theorem TopologicalSpace.IsSeparable.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)
          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)) :
          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.image {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [TopologicalSpace β] {s : Set α} (hs : TopologicalSpace.IsSeparable s) {f : αβ} (hf : Continuous f) :
          @[deprecated TopologicalSpace.IsSeparable.of_separableSpace]

          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 ι), (iF, 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 ι), (iF, 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 ι), (iF, U i T i) S = Set.pi (F) U}
          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 xx sx t) ∀ (x : α), IsTop xx sx t

          Let s be a dense set in a topological space α with partial order structure. If s is a separable space (e.g., if α has a second countable topology), then there exists a countable dense subset t ⊆ s such that t contains bottom/top element of α when they exist and belong to s. For a dense subset containing neither bot nor top elements, see Dense.exists_countable_dense_subset_no_bot_top.

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

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

          Instances
            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.instFirstCountableTopologyForAllTopologicalSpace {ι : Type u_1} {π : ιType u_2} [Countable ι] [(i : ι) → TopologicalSpace (π i)] [∀ (i : ι), FirstCountableTopology (π i)] :
            FirstCountableTopology ((i : ι) → π i)
            Equations
            • =

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

            Instances

              A countable topological basis of α.

              Equations
              Instances For

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

                instance TopologicalSpace.instSecondCountableTopologyForAllTopologicalSpace {ι : Type u_1} {π : ιType u_2} [Countable ι] [(a : ι) → TopologicalSpace (π a)] [∀ (a : ι), SecondCountableTopology (π a)] :
                SecondCountableTopology ((a : ι) → π a)
                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) :

                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 : iI, 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 : sS, 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 : xs, 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.

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

                Equations
                • =

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

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

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

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