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 TopologicalSpace.FirstCountableTopology, TopologicalSpace.SeparableSpace, and more.

structure TopologicalSpace.IsTopologicalBasis {α : Type u} [t : TopologicalSpace α] (s : Set (Set α)) :
  • 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).

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_open_of_nhds {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)} (h_open : ∀ (u : Set α), u sIsOpen u) (h_nhds : ∀ (a : α) (u : Set α), a uIsOpen uv, 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, 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 st, 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.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_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 BU 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 : ∀ (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 ba oSet.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 bSet.Nonempty oSet.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 BIsOpen (f '' s)
    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_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 BIsOpen (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 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.

    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_1} [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.

        instance TopologicalSpace.instSeparableSpaceForAllTopologicalSpace {ι : Type u_1} {X : ιType u_2} [(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 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 aIsOpen (s i)) (h'a : ∀ (i : ι), i aSet.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_1} {s : ιSet α} {a : Set ι} (h : Set.PairwiseDisjoint a s) (ha : ∀ (i : ι), i aSet.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 α] {ι : 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.image {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [TopologicalSpace β] {s : Set α} (hs : TopologicalSpace.IsSeparable s) {f : αβ} (hf : Continuous f) :
          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 FU 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 FU i T i) S = ⋂ (i : ι) (_ : i F), f i ⁻¹' U i}
          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 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.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 α] [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.

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

            Instances

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

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

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

              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.

              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.