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
    theorem ContinuousMap.continuous_toFun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (self : C(X, Y)) :
    Continuous self.toFun

    Proposition that toFun is continuous

    The type of continuous maps from X to Y.

    Equations
    • One or more equations did not get rendered due to their size.
    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
        theorem ContinuousMapClass.map_continuous {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} :
        ∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} {inst_2 : FunLike F X Y} [self : ContinuousMapClass F X Y] (f : F), Continuous f

        Continuity

        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
        • f = { toFun := f, continuous_toFun := }
        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
          • instCoeTCContinuousMap = { coe := toContinuousMap }

          Continuous maps #

          instance ContinuousMap.instFunLike {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
          FunLike C(X, Y) X Y
          Equations
          • ContinuousMap.instFunLike = { coe := ContinuousMap.toFun, coe_injective' := }
          @[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
          instance ContinuousMap.instCanLiftForallCoeContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] :
          CanLift (XY) C(X, Y) DFunLike.coe Continuous
          Equations
          • =
          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_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {g : C(X, Y)} :
            f = g ∀ (a : X), f a = g a
            theorem ContinuousMap.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {g : C(X, Y)} (h : ∀ (a : X), f a = g a) :
            f = g
            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
            • f.copy f' h = { toFun := f', continuous_toFun := }
            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.

              @[deprecated ContinuousMapClass.map_continuous]
              theorem ContinuousMap.continuous_set_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (s : Set C(X, Y)) (f : s) :
              Continuous f
              theorem ContinuousMap.congr_fun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {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 : 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