Documentation

Mathlib.Topology.Defs.Basic

Basic definitions about topological spaces #

This file contains definitions about topology that do not require imports other than Mathlib.Data.Set.Lattice.

Main definitions #

** Notation

We introduce notation IsOpen[t], IsClosed[t], closure[t], Continuous[t₁, t₂] that allow passing custom topologies to these predicates and functions without using @.

class TopologicalSpace (X : Type u) :

A topology on X.

Instances

    The set representing the whole space is an open set. Use isOpen_univ in the root namespace instead.

    The intersection of two open sets is an open set. Use IsOpen.inter instead.

    theorem TopologicalSpace.isOpen_sUnion {X : Type u} [self : TopologicalSpace X] (s : Set (Set X)) :

    The union of a family of open sets is an open set. Use isOpen_sUnion in the root namespace instead.

    Predicates on sets #

    def IsOpen {X : Type u} [TopologicalSpace X] :
    Set XProp

    IsOpen s means that s is open in the ambient topological space on X

    Equations
    • IsOpen = TopologicalSpace.IsOpen
    Instances For
      @[simp]
      theorem isOpen_univ {X : Type u} [TopologicalSpace X] :
      IsOpen Set.univ
      theorem IsOpen.inter {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsOpen s) (ht : IsOpen t) :
      IsOpen (s t)
      theorem isOpen_sUnion {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (h : ∀ (t : Set X), t sIsOpen t) :
      class IsClosed {X : Type u} [TopologicalSpace X] (s : Set X) :

      A set is closed if its complement is open

      • isOpen_compl : IsOpen s

        The complement of a closed set is an open set.

      Instances
        theorem IsClosed.isOpen_compl {X : Type u} [TopologicalSpace X] {s : Set X} [self : IsClosed s] :

        The complement of a closed set is an open set.

        def IsClopen {X : Type u} [TopologicalSpace X] (s : Set X) :

        A set is clopen if it is both closed and open.

        Equations
        Instances For
          def IsLocallyClosed {X : Type u} [TopologicalSpace X] (s : Set X) :

          A set is locally closed if it is the intersection of some open set and some closed set. Also see isLocallyClosed_tfae and other lemmas in Mathlib/Topology/LocallyClosed.

          Equations
          Instances For
            def interior {X : Type u} [TopologicalSpace X] (s : Set X) :
            Set X

            The interior of a set s is the largest open subset of s.

            Equations
            Instances For
              def closure {X : Type u} [TopologicalSpace X] (s : Set X) :
              Set X

              The closure of s is the smallest closed set containing s.

              Equations
              Instances For
                def frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
                Set X

                The frontier of a set is the set of points between the closure and interior.

                Equations
                Instances For
                  def coborder {X : Type u} [TopologicalSpace X] (s : Set X) :
                  Set X

                  The coborder is defined as the complement of closure s \ s, or the union of s and the complement of ∂(s). This is the largest set in which s is closed, and s is locally closed if and only if coborder s is open.

                  This is unnamed in the literature, and this name is due to the fact that coborder s = (border sᶜ)ᶜ where border s = s \ interior s is the border in the sense of Hausdorff.

                  Equations
                  Instances For
                    def Dense {X : Type u} [TopologicalSpace X] (s : Set X) :

                    A set is dense in a topological space if every point belongs to its closure.

                    Equations
                    Instances For
                      def DenseRange {X : Type u} [TopologicalSpace X] {α : Type u_1} (f : αX) :

                      f : α → X has dense range if its range (image) is a dense subset of X.

                      Equations
                      Instances For
                        structure Continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

                        A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.

                        • isOpen_preimage : ∀ (s : Set Y), IsOpen sIsOpen (f ⁻¹' s)

                          The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

                        Instances For
                          theorem Continuous.isOpen_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : Continuous f) (s : Set Y) :
                          IsOpen sIsOpen (f ⁻¹' s)

                          The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

                          def IsOpenMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

                          A map f : X → Y is said to be an open map, if the image of any open U : Set X is open in Y.

                          Equations
                          Instances For
                            def IsClosedMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

                            A map f : X → Y is said to be a closed map, if the image of any closed U : Set X is closed in Y.

                            Equations
                            Instances For
                              structure IsOpenQuotientMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) :

                              An open quotient map is an open map f : X → Y which is both an open map and a quotient map. Equivalently, it is a surjective continuous open map. We use the latter characterization as a definition.

                              Many important quotient maps are open quotient maps, including

                              • the quotient map from a topological space to its quotient by the action of a group;
                              • the quotient map from a topological group to its quotient by a normal subgroup;
                              • the quotient map from a topological spaace to its separation quotient.

                              Contrary to general quotient maps, the category of open quotient maps is closed under Prod.map.

                              Instances For

                                An open quotient map is surjective.

                                theorem IsOpenQuotientMap.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : IsOpenQuotientMap f) :

                                An open quotient map is continuous.

                                theorem IsOpenQuotientMap.isOpenMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (self : IsOpenQuotientMap f) :

                                An open quotient map is an open map.

                                Notation for non-standard topologies #

                                Notation for IsOpen with respect to a non-standard topology.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Notation for IsClosed with respect to a non-standard topology.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Notation for closure with respect to a non-standard topology.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Notation for Continuous with respect to a non-standard topologies.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        class BaireSpace (X : Type u_1) [TopologicalSpace X] :

                                        The property BaireSpace α means that the topological space α has the Baire property: any countable intersection of open dense subsets is dense. Formulated here when the source space is ℕ. Use dense_iInter_of_isOpen which works for any countable index type instead.

                                        Instances
                                          theorem BaireSpace.baire_property {X : Type u_1} [TopologicalSpace X] [self : BaireSpace X] (f : Set X) :
                                          (∀ (n : ), IsOpen (f n))(∀ (n : ), Dense (f n))Dense (⋂ (n : ), f n)