Documentation

Mathlib.Topology.Homotopy.Basic

Homotopy between functions #

In this file, we define a homotopy between two functions f₀ and f₁. First we define ContinuousMap.Homotopy between the two functions, with no restrictions on the intermediate maps. Then, as in the formalisation in HOL-Analysis, we define ContinuousMap.HomotopyWith f₀ f₁ P, for homotopies between f₀ and f₁, where the intermediate maps satisfy the predicate P. Finally, we define ContinuousMap.HomotopyRel f₀ f₁ S, for homotopies between f₀ and f₁ which are fixed on S.

Definitions #

For each of the above, we have

We also define the relations

and for ContinuousMap.homotopic and ContinuousMap.homotopic_rel, we also define the setoid and quotient in C(X, Y) by these relations.

References #

structure ContinuousMap.Homotopy {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) extends ContinuousMap :
Type (max u v)

ContinuousMap.Homotopy f₀ f₁ is the type of homotopies from f₀ to f₁.

When possible, instead of parametrizing results over (f : Homotopy f₀ f₁), you should parametrize over {F : Type*} [HomotopyLike F f₀ f₁] (f : F).

When you extend this structure, make sure to extend ContinuousMap.HomotopyLike.

  • toFun : unitInterval × XY
  • continuous_toFun : Continuous self.toFun
  • map_zero_left : ∀ (x : X), self.toFun (0, x) = f₀ x

    value of the homotopy at 0

  • map_one_left : ∀ (x : X), self.toFun (1, x) = f₁ x

    value of the homotopy at 1

Instances For
    theorem ContinuousMap.Homotopy.map_zero_left {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (self : f₀.Homotopy f₁) (x : X) :
    self.toFun (0, x) = f₀ x

    value of the homotopy at 0

    theorem ContinuousMap.Homotopy.map_one_left {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (self : f₀.Homotopy f₁) (x : X) :
    self.toFun (1, x) = f₁ x

    value of the homotopy at 1

    class ContinuousMap.HomotopyLike {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [TopologicalSpace X] [TopologicalSpace Y] (F : Type u_5) (f₀ : outParam C(X, Y)) (f₁ : outParam C(X, Y)) [FunLike F (unitInterval × X) Y] extends ContinuousMapClass :

    ContinuousMap.HomotopyLike F f₀ f₁ states that F is a type of homotopies between f₀ and f₁.

    You should extend this class when you extend ContinuousMap.Homotopy.

    • map_continuous : ∀ (f : F), Continuous f
    • map_zero_left : ∀ (f : F) (x : X), f (0, x) = f₀ x

      value of the homotopy at 0

    • map_one_left : ∀ (f : F) (x : X), f (1, x) = f₁ x

      value of the homotopy at 1

    Instances
      theorem ContinuousMap.HomotopyLike.map_zero_left {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_5} {f₀ : outParam C(X, Y)} {f₁ : outParam C(X, Y)} [FunLike F (unitInterval × X) Y] [self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X) :
      f (0, x) = f₀ x

      value of the homotopy at 0

      theorem ContinuousMap.HomotopyLike.map_one_left {X : outParam (Type u_3)} {Y : outParam (Type u_4)} [TopologicalSpace X] [TopologicalSpace Y] {F : Type u_5} {f₀ : outParam C(X, Y)} {f₁ : outParam C(X, Y)} [FunLike F (unitInterval × X) Y] [self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X) :
      f (1, x) = f₁ x

      value of the homotopy at 1

      instance ContinuousMap.Homotopy.instFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
      FunLike (f₀.Homotopy f₁) (unitInterval × X) Y
      Equations
      • ContinuousMap.Homotopy.instFunLike = { coe := fun (f : f₀.Homotopy f₁) => f.toFun, coe_injective' := }
      instance ContinuousMap.Homotopy.instHomotopyLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
      ContinuousMap.HomotopyLike (f₀.Homotopy f₁) f₀ f₁
      Equations
      • =
      theorem ContinuousMap.Homotopy.ext {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : f₀.Homotopy f₁} {G : f₀.Homotopy f₁} (h : ∀ (x : unitInterval × X), F x = G x) :
      F = G
      def ContinuousMap.Homotopy.Simps.apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :
      unitInterval × XY

      See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

      Equations
      Instances For
        theorem ContinuousMap.Homotopy.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :

        Deprecated. Use map_continuous instead.

        @[simp]
        theorem ContinuousMap.Homotopy.apply_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (x : X) :
        F (0, x) = f₀ x
        @[simp]
        theorem ContinuousMap.Homotopy.apply_one {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (x : X) :
        F (1, x) = f₁ x
        @[simp]
        theorem ContinuousMap.Homotopy.coe_toContinuousMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :
        F.toContinuousMap = F
        def ContinuousMap.Homotopy.curry {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :

        Currying a homotopy to a continuous function from I to C(X, Y).

        Equations
        • F.curry = F.curry
        Instances For
          @[simp]
          theorem ContinuousMap.Homotopy.curry_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (t : unitInterval) (x : X) :
          (F.curry t) x = F (t, x)
          def ContinuousMap.Homotopy.extend {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :

          Continuously extending a curried homotopy to a function from to C(X, Y).

          Equations
          Instances For
            theorem ContinuousMap.Homotopy.extend_apply_of_le_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {t : } (ht : t 0) (x : X) :
            (F.extend t) x = f₀ x
            theorem ContinuousMap.Homotopy.extend_apply_of_one_le {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {t : } (ht : 1 t) (x : X) :
            (F.extend t) x = f₁ x
            @[simp]
            theorem ContinuousMap.Homotopy.extend_apply_coe {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (t : unitInterval) (x : X) :
            (F.extend t) x = F (t, x)
            @[simp]
            theorem ContinuousMap.Homotopy.extend_apply_of_mem_I {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {t : } (ht : t unitInterval) (x : X) :
            (F.extend t) x = F (t, ht, x)
            theorem ContinuousMap.Homotopy.congr_fun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : f₀.Homotopy f₁} {G : f₀.Homotopy f₁} (h : F = G) (x : unitInterval × X) :
            F x = G x
            theorem ContinuousMap.Homotopy.congr_arg {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {x : unitInterval × X} {y : unitInterval × X} (h : x = y) :
            F x = F y
            def ContinuousMap.Homotopy.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
            f.Homotopy f

            Given a continuous function f, we can define a Homotopy f f by F (t, x) = f x

            Equations
            Instances For
              Equations
              @[simp]
              theorem ContinuousMap.Homotopy.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (x : unitInterval × X) :
              F.symm x = F (unitInterval.symm x.1, x.2)
              def ContinuousMap.Homotopy.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :
              f₁.Homotopy f₀

              Given a Homotopy f₀ f₁, we can define a Homotopy f₁ f₀ by reversing the homotopy.

              Equations
              Instances For
                @[simp]
                theorem ContinuousMap.Homotopy.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :
                F.symm.symm = F
                theorem ContinuousMap.Homotopy.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
                Function.Bijective ContinuousMap.Homotopy.symm
                def ContinuousMap.Homotopy.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) :
                f₀.Homotopy f₂

                Given Homotopy f₀ f₁ and Homotopy f₁ f₂, we can define a Homotopy f₀ f₂ by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem ContinuousMap.Homotopy.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) (x : unitInterval × X) :
                  (F.trans G) x = if h : x.1 1 / 2 then F (2 * x.1, , x.2) else G (2 * x.1 - 1, , x.2)
                  theorem ContinuousMap.Homotopy.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) :
                  (F.trans G).symm = G.symm.trans F.symm
                  @[simp]
                  theorem ContinuousMap.Homotopy.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.Homotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : unitInterval × X) :
                  (F.cast h₀ h₁) a = F a
                  def ContinuousMap.Homotopy.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.Homotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
                  g₀.Homotopy g₁

                  Casting a Homotopy f₀ f₁ to a Homotopy g₀ g₁ where f₀ = g₀ and f₁ = g₁.

                  Equations
                  • F.cast h₀ h₁ = { toFun := F, continuous_toFun := , map_zero_left := , map_one_left := }
                  Instances For
                    @[simp]
                    theorem ContinuousMap.Homotopy.compContinuousMap_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (f : C(X, Y)) :
                    ∀ (a : unitInterval × X), (G.compContinuousMap f) a = G (a.1, f a.2)
                    def ContinuousMap.Homotopy.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (f : C(X, Y)) :
                    (g₀.comp f).Homotopy (g₁.comp f)

                    Composition of a Homotopy g₀ g₁ and f : C(X, Y) as a homotopy between g₀.comp f and g₁.comp f.

                    Equations
                    Instances For
                      @[simp]
                      theorem ContinuousMap.Homotopy.hcomp_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) (x : unitInterval × X) :
                      (F.hcomp G) x = G (x.1, F x)
                      def ContinuousMap.Homotopy.hcomp {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) :
                      (g₀.comp f₀).Homotopy (g₁.comp f₁)

                      If we have a Homotopy f₀ f₁ and a Homotopy g₀ g₁, then we can compose them and get a Homotopy (g₀.comp f₀) (g₁.comp f₁).

                      Equations
                      • F.hcomp G = { toFun := fun (x : unitInterval × X) => G (x.1, F x), continuous_toFun := , map_zero_left := , map_one_left := }
                      Instances For
                        def ContinuousMap.Homotopy.prodMk {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Z)} {g₁ : C(X, Z)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) :
                        (f₀.prodMk g₀).Homotopy (f₁.prodMk g₁)

                        Let F be a homotopy between f₀ : C(X, Y) and f₁ : C(X, Y). Let G be a homotopy between g₀ : C(X, Z) and g₁ : C(X, Z). Then F.prodMk G is the homotopy between f₀.prodMk g₀ and f₁.prodMk g₁ that sends p to (F p, G p).

                        Equations
                        • F.prodMk G = { toContinuousMap := F.prodMk G, map_zero_left := , map_one_left := }
                        Instances For
                          def ContinuousMap.Homotopy.prodMap {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Z, Z')} {g₁ : C(Z, Z')} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁) :
                          (f₀.prodMap g₀).Homotopy (f₁.prodMap g₁)

                          Let F be a homotopy between f₀ : C(X, Y) and f₁ : C(X, Y). Let G be a homotopy between g₀ : C(Z, Z') and g₁ : C(Z, Z'). Then F.prodMap G is the homotopy between f₀.prodMap g₀ and f₁.prodMap g₁ that sends (t, x, z) to (F (t, x), G (t, z)).

                          Equations
                          Instances For
                            def ContinuousMap.Homotopy.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ιType u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : (i : ι) → (f₀ i).Homotopy (f₁ i)) :
                            (ContinuousMap.pi f₀).Homotopy (ContinuousMap.pi f₁)

                            Given a family of homotopies F i between f₀ i : C(X, Y i) and f₁ i : C(X, Y i), returns a homotopy between ContinuousMap.pi f₀ and ContinuousMap.pi f₁.

                            Equations
                            Instances For
                              def ContinuousMap.Homotopy.piMap {ι : Type u_2} {X : ιType u_3} {Y : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X i, Y i)} {f₁ : (i : ι) → C(X i, Y i)} (F : (i : ι) → (f₀ i).Homotopy (f₁ i)) :

                              Given a family of homotopies F i between f₀ i : C(X i, Y i) and f₁ i : C(X i, Y i), returns a homotopy between ContinuousMap.piMap f₀ and ContinuousMap.piMap f₁.

                              Equations
                              Instances For
                                def ContinuousMap.Homotopic {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) :

                                Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic if there exists a Homotopy f₀ f₁.

                                Equations
                                • f₀.Homotopic f₁ = Nonempty (f₀.Homotopy f₁)
                                Instances For
                                  theorem ContinuousMap.Homotopic.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) :
                                  f.Homotopic f
                                  theorem ContinuousMap.Homotopic.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] ⦃f : C(X, Y) ⦃g : C(X, Y) (h : f.Homotopic g) :
                                  g.Homotopic f
                                  theorem ContinuousMap.Homotopic.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] ⦃f : C(X, Y) ⦃g : C(X, Y) ⦃h : C(X, Y) (h₀ : f.Homotopic g) (h₁ : g.Homotopic h) :
                                  f.Homotopic h
                                  theorem ContinuousMap.Homotopic.hcomp {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (h₀ : f₀.Homotopic f₁) (h₁ : g₀.Homotopic g₁) :
                                  (g₀.comp f₀).Homotopic (g₁.comp f₁)
                                  theorem ContinuousMap.Homotopic.equivalence {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] :
                                  Equivalence ContinuousMap.Homotopic
                                  theorem ContinuousMap.Homotopic.prodMk {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Z)} {g₁ : C(X, Z)} :
                                  f₀.Homotopic f₁g₀.Homotopic g₁(f₀.prodMk g₀).Homotopic (f₁.prodMk g₁)
                                  theorem ContinuousMap.Homotopic.prodMap {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z'] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(Z, Z')} {g₁ : C(Z, Z')} :
                                  f₀.Homotopic f₁g₀.Homotopic g₁(f₀.prodMap g₀).Homotopic (f₁.prodMap g₁)
                                  theorem ContinuousMap.Homotopic.pi {X : Type u} {ι : Type u_2} [TopologicalSpace X] {Y : ιType u_3} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)) :
                                  (ContinuousMap.pi f₀).Homotopic (ContinuousMap.pi f₁)

                                  If each f₀ i : C(X, Y i) is homotopic to f₁ i : C(X, Y i), then ContinuousMap.pi f₀ is homotopic to ContinuousMap.pi f₁.

                                  theorem ContinuousMap.Homotopic.piMap {ι : Type u_2} {X : ιType u_3} {Y : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X i, Y i)} {f₁ : (i : ι) → C(X i, Y i)} (F : ∀ (i : ι), (f₀ i).Homotopic (f₁ i)) :

                                  If each f₀ i : C(X, Y i) is homotopic to f₁ i : C(X, Y i), then ContinuousMap.pi f₀ is homotopic to ContinuousMap.pi f₁.

                                  structure ContinuousMap.HomotopyWith {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (P : C(X, Y)Prop) extends ContinuousMap.Homotopy :
                                  Type (max u v)

                                  The type of homotopies between f₀ f₁ : C(X, Y), where the intermediate maps satisfy the predicate P : C(X, Y) → Prop

                                  • toFun : unitInterval × XY
                                  • continuous_toFun : Continuous self.toFun
                                  • map_zero_left : ∀ (x : X), self.toFun (0, x) = f₀ x
                                  • map_one_left : ∀ (x : X), self.toFun (1, x) = f₁ x
                                  • prop' : ∀ (t : unitInterval), P { toFun := fun (x : X) => self.toFun (t, x), continuous_toFun := }

                                    the intermediate maps of the homotopy satisfy the property

                                  Instances For
                                    theorem ContinuousMap.HomotopyWith.prop' {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (self : f₀.HomotopyWith f₁ P) (t : unitInterval) :
                                    P { toFun := fun (x : X) => self.toFun (t, x), continuous_toFun := }

                                    the intermediate maps of the homotopy satisfy the property

                                    instance ContinuousMap.HomotopyWith.instFunLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} :
                                    FunLike (f₀.HomotopyWith f₁ P) (unitInterval × X) Y
                                    Equations
                                    • ContinuousMap.HomotopyWith.instFunLike = { coe := fun (F : f₀.HomotopyWith f₁ P) => F.toHomotopy, coe_injective' := }
                                    instance ContinuousMap.HomotopyWith.instHomotopyLike {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} :
                                    ContinuousMap.HomotopyLike (f₀.HomotopyWith f₁ P) f₀ f₁
                                    Equations
                                    • =
                                    theorem ContinuousMap.HomotopyWith.coeFn_injective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} :
                                    Function.Injective DFunLike.coe
                                    theorem ContinuousMap.HomotopyWith.ext {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} {F : f₀.HomotopyWith f₁ P} {G : f₀.HomotopyWith f₁ P} (h : ∀ (x : unitInterval × X), F x = G x) :
                                    F = G
                                    def ContinuousMap.HomotopyWith.Simps.apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) :
                                    unitInterval × XY

                                    See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

                                    Equations
                                    Instances For
                                      theorem ContinuousMap.HomotopyWith.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) :
                                      @[simp]
                                      theorem ContinuousMap.HomotopyWith.apply_zero {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) (x : X) :
                                      F (0, x) = f₀ x
                                      @[simp]
                                      theorem ContinuousMap.HomotopyWith.apply_one {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) (x : X) :
                                      F (1, x) = f₁ x
                                      theorem ContinuousMap.HomotopyWith.coe_toContinuousMap {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) :
                                      F.toContinuousMap = F
                                      @[simp]
                                      theorem ContinuousMap.HomotopyWith.coe_toHomotopy {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) :
                                      F.toHomotopy = F
                                      theorem ContinuousMap.HomotopyWith.prop {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) (t : unitInterval) :
                                      P (F.curry t)
                                      theorem ContinuousMap.HomotopyWith.extendProp {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) (t : ) :
                                      P (F.extend t)
                                      @[simp]
                                      theorem ContinuousMap.HomotopyWith.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) (x : unitInterval × X) :
                                      @[simp]
                                      theorem ContinuousMap.HomotopyWith.refl_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) (x : unitInterval × X) :
                                      def ContinuousMap.HomotopyWith.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) :
                                      f.HomotopyWith f P

                                      Given a continuous function f, and a proof h : P f, we can define a HomotopyWith f f P by F (t, x) = f x

                                      Equations
                                      Instances For
                                        Equations
                                        @[simp]
                                        theorem ContinuousMap.HomotopyWith.symm_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (x : unitInterval × X) :
                                        F.symm x = F (unitInterval.symm x.1, x.2)
                                        @[simp]
                                        theorem ContinuousMap.HomotopyWith.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (x : unitInterval × X) :
                                        F.symm x = F (unitInterval.symm x.1, x.2)
                                        def ContinuousMap.HomotopyWith.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) :
                                        f₁.HomotopyWith f₀ P

                                        Given a HomotopyWith f₀ f₁ P, we can define a HomotopyWith f₁ f₀ P by reversing the homotopy.

                                        Equations
                                        • F.symm = { toHomotopy := F.symm, prop' := }
                                        Instances For
                                          @[simp]
                                          theorem ContinuousMap.HomotopyWith.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) :
                                          F.symm.symm = F
                                          theorem ContinuousMap.HomotopyWith.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
                                          Function.Bijective ContinuousMap.HomotopyWith.symm
                                          def ContinuousMap.HomotopyWith.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (G : f₁.HomotopyWith f₂ P) :
                                          f₀.HomotopyWith f₂ P

                                          Given HomotopyWith f₀ f₁ P and HomotopyWith f₁ f₂ P, we can define a HomotopyWith f₀ f₂ P by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].

                                          Equations
                                          • F.trans G = let __src := F.trans G.toHomotopy; { toHomotopy := __src, prop' := }
                                          Instances For
                                            theorem ContinuousMap.HomotopyWith.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (G : f₁.HomotopyWith f₂ P) (x : unitInterval × X) :
                                            (F.trans G) x = if h : x.1 1 / 2 then F (2 * x.1, , x.2) else G (2 * x.1 - 1, , x.2)
                                            theorem ContinuousMap.HomotopyWith.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (G : f₁.HomotopyWith f₂ P) :
                                            (F.trans G).symm = G.symm.trans F.symm
                                            @[simp]
                                            theorem ContinuousMap.HomotopyWith.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : unitInterval × X) :
                                            (F.cast h₀ h₁) a = F a
                                            @[simp]
                                            theorem ContinuousMap.HomotopyWith.cast_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : unitInterval × X) :
                                            (F.cast h₀ h₁) a = F a
                                            def ContinuousMap.HomotopyWith.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
                                            g₀.HomotopyWith g₁ P

                                            Casting a HomotopyWith f₀ f₁ P to a HomotopyWith g₀ g₁ P where f₀ = g₀ and f₁ = g₁.

                                            Equations
                                            • F.cast h₀ h₁ = { toHomotopy := F.cast h₀ h₁, prop' := }
                                            Instances For
                                              def ContinuousMap.HomotopicWith {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (P : C(X, Y)Prop) :

                                              Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic with respect to the predicate P if there exists a HomotopyWith f₀ f₁ P.

                                              Equations
                                              • f₀.HomotopicWith f₁ P = Nonempty (f₀.HomotopyWith f₁ P)
                                              Instances For
                                                theorem ContinuousMap.HomotopicWith.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) :
                                                f.HomotopicWith f P
                                                theorem ContinuousMap.HomotopicWith.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} ⦃f : C(X, Y) ⦃g : C(X, Y) (h : f.HomotopicWith g P) :
                                                g.HomotopicWith f P
                                                theorem ContinuousMap.HomotopicWith.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {P : C(X, Y)Prop} ⦃f : C(X, Y) ⦃g : C(X, Y) ⦃h : C(X, Y) (h₀ : f.HomotopicWith g P) (h₁ : g.HomotopicWith h P) :
                                                f.HomotopicWith h P
                                                @[reducible, inline]
                                                abbrev ContinuousMap.HomotopyRel {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (S : Set X) :
                                                Type (max u v)

                                                A HomotopyRel f₀ f₁ S is a homotopy between f₀ and f₁ which is fixed on the points in S.

                                                Equations
                                                • f₀.HomotopyRel f₁ S = f₀.HomotopyWith f₁ fun (f : C(X, Y)) => xS, f x = f₀ x
                                                Instances For
                                                  theorem ContinuousMap.HomotopyRel.eq_fst {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (t : unitInterval) {x : X} (hx : x S) :
                                                  F (t, x) = f₀ x
                                                  theorem ContinuousMap.HomotopyRel.eq_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (t : unitInterval) {x : X} (hx : x S) :
                                                  F (t, x) = f₁ x
                                                  theorem ContinuousMap.HomotopyRel.fst_eq_snd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) {x : X} (hx : x S) :
                                                  f₀ x = f₁ x
                                                  @[simp]
                                                  @[simp]
                                                  def ContinuousMap.HomotopyRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) :
                                                  f.HomotopyRel f S

                                                  Given a map f : C(X, Y) and a set S, we can define a HomotopyRel f f S by setting F (t, x) = f x for all t. This is defined using HomotopyWith.refl, but with the proof filled in.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem ContinuousMap.HomotopyRel.symm_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (x : unitInterval × X) :
                                                    F.symm x = F (unitInterval.symm x.1, x.2)
                                                    @[simp]
                                                    theorem ContinuousMap.HomotopyRel.symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (x : unitInterval × X) :
                                                    F.symm x = F (unitInterval.symm x.1, x.2)
                                                    def ContinuousMap.HomotopyRel.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) :
                                                    f₁.HomotopyRel f₀ S

                                                    Given a HomotopyRel f₀ f₁ S, we can define a HomotopyRel f₁ f₀ S by reversing the homotopy.

                                                    Equations
                                                    • F.symm = { toHomotopy := F.symm, prop' := }
                                                    Instances For
                                                      @[simp]
                                                      theorem ContinuousMap.HomotopyRel.symm_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) :
                                                      F.symm.symm = F
                                                      theorem ContinuousMap.HomotopyRel.symm_bijective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} :
                                                      Function.Bijective ContinuousMap.HomotopyRel.symm
                                                      def ContinuousMap.HomotopyRel.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (G : f₁.HomotopyRel f₂ S) :
                                                      f₀.HomotopyRel f₂ S

                                                      Given HomotopyRel f₀ f₁ S and HomotopyRel f₁ f₂ S, we can define a HomotopyRel f₀ f₂ S by putting the first homotopy on [0, 1/2] and the second on [1/2, 1].

                                                      Equations
                                                      • F.trans G = { toHomotopy := F.trans G.toHomotopy, prop' := }
                                                      Instances For
                                                        theorem ContinuousMap.HomotopyRel.trans_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (G : f₁.HomotopyRel f₂ S) (x : unitInterval × X) :
                                                        (F.trans G) x = if h : x.1 1 / 2 then F (2 * x.1, , x.2) else G (2 * x.1 - 1, , x.2)
                                                        theorem ContinuousMap.HomotopyRel.symm_trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (G : f₁.HomotopyRel f₂ S) :
                                                        (F.trans G).symm = G.symm.trans F.symm
                                                        @[simp]
                                                        theorem ContinuousMap.HomotopyRel.cast_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : unitInterval × X) :
                                                        (F.cast h₀ h₁) a = F a
                                                        @[simp]
                                                        theorem ContinuousMap.HomotopyRel.cast_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : unitInterval × X) :
                                                        (F.cast h₀ h₁) a = F a
                                                        def ContinuousMap.HomotopyRel.cast {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} {g₀ : C(X, Y)} {g₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
                                                        g₀.HomotopyRel g₁ S

                                                        Casting a HomotopyRel f₀ f₁ S to a HomotopyRel g₀ g₁ S where f₀ = g₀ and f₁ = g₁.

                                                        Equations
                                                        • F.cast h₀ h₁ = { toHomotopy := F.cast h₀ h₁, prop' := }
                                                        Instances For
                                                          @[simp]
                                                          theorem ContinuousMap.HomotopyRel.compContinuousMap_toFun {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) (x : unitInterval × X) :
                                                          (F.compContinuousMap g) x = g (F x)
                                                          @[simp]
                                                          theorem ContinuousMap.HomotopyRel.compContinuousMap_apply {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) (x : unitInterval × X) :
                                                          (F.compContinuousMap g) x = g (F x)
                                                          def ContinuousMap.HomotopyRel.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) :
                                                          (g.comp f₀).HomotopyRel (g.comp f₁) S

                                                          Post-compose a homotopy relative to a set by a continuous function.

                                                          Equations
                                                          Instances For
                                                            def ContinuousMap.HomotopicRel {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (S : Set X) :

                                                            Given continuous maps f₀ and f₁, we say f₀ and f₁ are homotopic relative to a set S if there exists a HomotopyRel f₀ f₁ S.

                                                            Equations
                                                            • f₀.HomotopicRel f₁ S = Nonempty (f₀.HomotopyRel f₁ S)
                                                            Instances For
                                                              theorem ContinuousMap.HomotopicRel.homotopic {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (h : f₀.HomotopicRel f₁ S) :
                                                              f₀.Homotopic f₁

                                                              If two maps are homotopic relative to a set, then they are homotopic.

                                                              theorem ContinuousMap.HomotopicRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} (f : C(X, Y)) :
                                                              f.HomotopicRel f S
                                                              theorem ContinuousMap.HomotopicRel.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} ⦃f : C(X, Y) ⦃g : C(X, Y) (h : f.HomotopicRel g S) :
                                                              g.HomotopicRel f S
                                                              theorem ContinuousMap.HomotopicRel.trans {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} ⦃f : C(X, Y) ⦃g : C(X, Y) ⦃h : C(X, Y) (h₀ : f.HomotopicRel g S) (h₁ : g.HomotopicRel h S) :
                                                              f.HomotopicRel h S
                                                              theorem ContinuousMap.HomotopicRel.equivalence {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} :
                                                              Equivalence fun (f g : C(X, Y)) => f.HomotopicRel g S
                                                              @[simp]
                                                              theorem ContinuousMap.homotopicRel_empty {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
                                                              f₀.HomotopicRel f₁ f₀.Homotopic f₁