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

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

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

                                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