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

                          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)