Documentation

Mathlib.Topology.ContinuousMap.Defs

Continuous bundled maps #

In this file we define the type ContinuousMap of continuous bundled maps.

We use the DFunLike design, so each type of morphisms has a companion typeclass which is meant to be satisfied by itself and all stricter types.

structure ContinuousMap (X : Type u_1) (Y : Type u_2) [TopologicalSpace X] [TopologicalSpace Y] :
Type (max u_1 u_2)

The type of continuous maps from X to Y.

When possible, instead of parametrizing results over (f : C(X, Y)), you should parametrize over {F : Type*} [ContinuousMapClass F X Y] (f : F).

When you extend this structure, make sure to extend ContinuousMapClass.

  • toFun : XY

    The function X → Y

  • continuous_toFun : Continuous self.toFun

    Proposition that toFun is continuous

Instances For

    C(X, Y) is the type of continuous maps from X to Y.

    Equations
      Instances For
        class ContinuousMapClass (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] :

        ContinuousMapClass F X Y states that F is a type of continuous maps.

        You should extend this class when you extend ContinuousMap.

        • map_continuous (f : F) : Continuous f

          Continuity

        Instances
          def toContinuousMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) :
          C(X, Y)

          Coerce a bundled morphism with a ContinuousMapClass instance to a ContinuousMap.

          Equations
            Instances For
              instance instCoeTCContinuousMap {F : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [FunLike F X Y] [ContinuousMapClass F X Y] :
              CoeTC F C(X, Y)
              Equations

                Continuous maps #

                instance ContinuousMap.instFunLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
                FunLike C(X, Y) X Y
                Equations
                  @[simp]
                  theorem ContinuousMap.toFun_eq_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} :
                  f.toFun = f
                  def ContinuousMap.Simps.apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
                  XY

                  See note [custom simps projection].

                  Equations
                    Instances For
                      @[simp]
                      theorem ContinuousMap.coe_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) :
                      f = f
                      theorem ContinuousMap.coe_apply {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_3} [FunLike F X Y] [ContinuousMapClass F X Y] (f : F) (x : X) :
                      f x = f x
                      theorem ContinuousMap.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (h : ∀ (a : X), f a = g a) :
                      f = g
                      theorem ContinuousMap.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} :
                      f = g ∀ (a : X), f a = g a
                      def ContinuousMap.copy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : XY) (h : f' = f) :
                      C(X, Y)

                      Copy of a ContinuousMap with a new toFun equal to the old one. Useful to fix definitional equalities.

                      Equations
                        Instances For
                          @[simp]
                          theorem ContinuousMap.coe_copy {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : XY) (h : f' = f) :
                          (f.copy f' h) = f'
                          theorem ContinuousMap.copy_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (f' : XY) (h : f' = f) :
                          f.copy f' h = f
                          theorem ContinuousMap.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :

                          Deprecated. Use map_continuous instead.

                          theorem ContinuousMap.congr_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)} (H : f = g) (x : X) :
                          f x = g x

                          Deprecated. Use DFunLike.congr_fun instead.

                          theorem ContinuousMap.congr_arg {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) {x y : X} (h : x = y) :
                          f x = f y

                          Deprecated. Use DFunLike.congr_arg instead.

                          @[simp]
                          theorem ContinuousMap.coe_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (h : Continuous f) :
                          { toFun := f, continuous_toFun := h } = f