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

• ContinuousMap.Homotopy f₀ f₁ is the type of homotopies between f₀ and f₁.
• ContinuousMap.HomotopyWith f₀ f₁ P is the type of homotopies between f₀ and f₁, where the intermediate maps satisfy the predicate P.
• ContinuousMap.HomotopyRel f₀ f₁ S is the type of homotopies between f₀ and f₁ which are fixed on S.

For each of the above, we have

• refl f, which is the constant homotopy from f to f.
• symm F, which reverses the homotopy F. For example, if F : ContinuousMap.Homotopy f₀ f₁, then F.symm : ContinuousMap.Homotopy f₁ f₀.
• trans F G, which concatenates the homotopies F and G. For example, if F : ContinuousMap.Homotopy f₀ f₁ and G : ContinuousMap.Homotopy f₁ f₂, then F.trans G : ContinuousMap.Homotopy f₀ f₂.

We also define the relations

• ContinuousMap.Homotopic f₀ f₁ is defined to be Nonempty (ContinuousMap.Homotopy f₀ f₁)
• ContinuousMap.HomotopicWith f₀ f₁ P is defined to be Nonempty (ContinuousMap.HomotopyWith f₀ f₁ P)
• ContinuousMap.HomotopicRel f₀ f₁ P is defined to be Nonempty (ContinuousMap.HomotopyRel f₀ f₁ P)

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

References

• HOL-Analysis formalisation

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)

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous s.toFun
• map_zero_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (0, x) = ↑f₀ x

  value of the homotopy at 0

• map_one_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (1, x) = ↑f₁ x

  value of the homotopy at 1

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.

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

• coe : F → ↑unitInterval × X → Y
• coe_injective' : Function.Injective FunLike.coe
• 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

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.

instance ContinuousMap.Homotopy.instHomotopyLikeHomotopy {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} : ContinuousMap.HomotopyLike (ContinuousMap.Homotopy f₀ f₁) f₀ f₁

theorem ContinuousMap.Homotopy.ext {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : ContinuousMap.Homotopy f₀ f₁} {G : ContinuousMap.Homotopy f₀ 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 : ContinuousMap.Homotopy f₀ f₁) : ↑unitInterval × X → Y

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

theorem ContinuousMap.Homotopy.continuous {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : Continuous ↑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 : ContinuousMap.Homotopy f₀ 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 : ContinuousMap.Homotopy f₀ 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 : ContinuousMap.Homotopy f₀ 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 : ContinuousMap.Homotopy f₀ f₁) : C(↑unitInterval, C(X, Y))

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

@[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 : ContinuousMap.Homotopy f₀ f₁) (t : ↑unitInterval) (x : X) : ↑(↑(ContinuousMap.Homotopy.curry F) 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 : ContinuousMap.Homotopy f₀ f₁) : C(ℝ, C(X, Y))

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

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 : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : t ≤ 0) (x : X) : ↑(↑(ContinuousMap.Homotopy.extend F) 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 : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : 1 ≤ t) (x : X) : ↑(↑(ContinuousMap.Homotopy.extend F) 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 : ContinuousMap.Homotopy f₀ f₁) (t : ↑unitInterval) (x : X) : ↑(↑(ContinuousMap.Homotopy.extend F) ↑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 : ContinuousMap.Homotopy f₀ f₁) {t : ℝ} (ht : t ∈ unitInterval) (x : X) : ↑(↑(ContinuousMap.Homotopy.extend F) t) x = ↑F ({ val := t, property := 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 : ContinuousMap.Homotopy f₀ f₁} {G : ContinuousMap.Homotopy f₀ 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 : ContinuousMap.Homotopy f₀ f₁) {x : ↑unitInterval × X} {y : ↑unitInterval × X} (h : x = y) : ↑F x = ↑F y

@[simp]

theorem ContinuousMap.Homotopy.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (x : ↑unitInterval × X) : ↑(ContinuousMap.Homotopy.refl f) x = ↑f x.snd

def ContinuousMap.Homotopy.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : ContinuousMap.Homotopy f f

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

instance ContinuousMap.Homotopy.instInhabitedHomotopyId {X : Type u} [TopologicalSpace X] : Inhabited (ContinuousMap.Homotopy (ContinuousMap.id X) (ContinuousMap.id X))

@[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 : ContinuousMap.Homotopy f₀ f₁) (x : ↑unitInterval × X) : ↑(ContinuousMap.Homotopy.symm F) x = ↑F (unitInterval.symm x.fst, x.snd)

def ContinuousMap.Homotopy.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : ContinuousMap.Homotopy f₀ f₁) : ContinuousMap.Homotopy f₁ f₀

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

@[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 : ContinuousMap.Homotopy f₀ f₁) : ContinuousMap.Homotopy.symm (ContinuousMap.Homotopy.symm F) = F

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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) : ContinuousMap.Homotopy f₀ 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].

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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) (x : ↑unitInterval × X) : ↑(ContinuousMap.Homotopy.trans F G) x = if h : ↑x.fst ≤ 1 / 2 then ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ unitInterval) }, x.snd) else ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ unitInterval) }, x.snd)

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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy f₁ f₂) : ContinuousMap.Homotopy.symm (ContinuousMap.Homotopy.trans F G) = ContinuousMap.Homotopy.trans (ContinuousMap.Homotopy.symm G) (ContinuousMap.Homotopy.symm F)

@[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 : ContinuousMap.Homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : ↑(ContinuousMap.Homotopy.cast F 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 : ContinuousMap.Homotopy f₀ f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.Homotopy g₀ g₁

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

@[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 : ContinuousMap.Homotopy g₀ g₁) (f : C(X, Y)) : ∀ (a : ↑unitInterval × X), ↑(ContinuousMap.Homotopy.compContinuousMap G f) a = ↑G (a.fst, ↑f a.snd)

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 : ContinuousMap.Homotopy g₀ g₁) (f : C(X, Y)) : ContinuousMap.Homotopy (ContinuousMap.comp g₀ f) (ContinuousMap.comp g₁ f)

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

@[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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) (x : ↑unitInterval × X) : ↑(ContinuousMap.Homotopy.hcomp F G) x = ↑G (x.fst, ↑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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.comp g₀ f₀) (ContinuousMap.comp g₁ 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₁).

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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.prodMk f₀ g₀) (ContinuousMap.prodMk f₁ 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).

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 : ContinuousMap.Homotopy f₀ f₁) (G : ContinuousMap.Homotopy g₀ g₁) : ContinuousMap.Homotopy (ContinuousMap.prodMap f₀ g₀) (ContinuousMap.prodMap f₁ 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)).

def ContinuousMap.Homotopy.pi {X : Type u} [TopologicalSpace X] {ι : Type u_3} {Y : ι → Type u_2} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : (i : ι) → ContinuousMap.Homotopy (f₀ i) (f₁ i)) : ContinuousMap.Homotopy (ContinuousMap.pi f₀) (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₁.

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

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

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

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

theorem ContinuousMap.Homotopic.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : ContinuousMap.Homotopic f f

theorem ContinuousMap.Homotopic.symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] ⦃f : C(X, Y)⦄ ⦃g : C(X, Y)⦄ (h : ContinuousMap.Homotopic f g) : ContinuousMap.Homotopic g 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₀ : ContinuousMap.Homotopic f g) (h₁ : ContinuousMap.Homotopic g h) : ContinuousMap.Homotopic f 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₀ : ContinuousMap.Homotopic f₀ f₁) (h₁ : ContinuousMap.Homotopic g₀ g₁) : ContinuousMap.Homotopic (ContinuousMap.comp g₀ f₀) (ContinuousMap.comp g₁ 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)} : ContinuousMap.Homotopic f₀ f₁ → ContinuousMap.Homotopic g₀ g₁ → ContinuousMap.Homotopic (ContinuousMap.prodMk f₀ g₀) (ContinuousMap.prodMk f₁ 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')} : ContinuousMap.Homotopic f₀ f₁ → ContinuousMap.Homotopic g₀ g₁ → ContinuousMap.Homotopic (ContinuousMap.prodMap f₀ g₀) (ContinuousMap.prodMap f₁ g₁)

theorem ContinuousMap.Homotopic.pi {X : Type u} [TopologicalSpace X] {ι : Type u_3} {Y : ι → Type u_2} [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X, Y i)} {f₁ : (i : ι) → C(X, Y i)} (F : ∀ (i : ι), ContinuousMap.Homotopic (f₀ i) (f₁ i)) : ContinuousMap.Homotopic (ContinuousMap.pi f₀) (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_4} {X : ι → Type u_2} {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (X i)] [(i : ι) → TopologicalSpace (Y i)] {f₀ : (i : ι) → C(X i, Y i)} {f₁ : (i : ι) → C(X i, Y i)} (F : ∀ (i : ι), ContinuousMap.Homotopic (f₀ i) (f₁ i)) : ContinuousMap.Homotopic (ContinuousMap.piMap f₀) (ContinuousMap.piMap 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₁.

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)

• toFun : ↑unitInterval × X → Y
• continuous_toFun : Continuous s.toFun
• map_zero_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (0, x) = ↑f₀ x
• map_one_left : ∀ (x : X), ContinuousMap.toFun s.toContinuousMap (1, x) = ↑f₁ x
• prop' : ∀ (t : ↑unitInterval), P (ContinuousMap.mk fun x => ContinuousMap.toFun s.toContinuousMap (t, x))

  the intermediate maps of the homotopy satisfy the property

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

instance ContinuousMap.HomotopyWith.instHomotopyLikeHomotopyWith {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 (ContinuousMap.HomotopyWith f₀ f₁ P) f₀ f₁

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 FunLike.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 : ContinuousMap.HomotopyWith f₀ f₁ P} {G : ContinuousMap.HomotopyWith f₀ 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 : ContinuousMap.HomotopyWith f₀ f₁ P) : ↑unitInterval × X → Y

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

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 : ContinuousMap.HomotopyWith f₀ f₁ P) : Continuous ↑F

@[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 : ContinuousMap.HomotopyWith f₀ 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 : ContinuousMap.HomotopyWith f₀ 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 : ContinuousMap.HomotopyWith f₀ 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 : ContinuousMap.HomotopyWith f₀ 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 : ContinuousMap.HomotopyWith f₀ f₁ P) (t : ↑unitInterval) : P (↑(ContinuousMap.Homotopy.curry F.toHomotopy) 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 : ContinuousMap.HomotopyWith f₀ f₁ P) (t : ℝ) : P (↑(ContinuousMap.Homotopy.extend F.toHomotopy) t)

@[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) : ↑(ContinuousMap.HomotopyWith.refl f hf) x = ↑f x.snd

@[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) : ↑(ContinuousMap.HomotopyWith.refl f hf) x = ↑f x.snd

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) : ContinuousMap.HomotopyWith f 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

instance ContinuousMap.HomotopyWith.instInhabitedHomotopyWithIdContinuousMapTrue {X : Type u} [TopologicalSpace X] : Inhabited (ContinuousMap.HomotopyWith (ContinuousMap.id X) (ContinuousMap.id X) fun x => True)

@[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 : ContinuousMap.HomotopyWith f₀ f₁ P) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyWith.symm F) x = ↑F (unitInterval.symm x.fst, x.snd)

@[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 : ContinuousMap.HomotopyWith f₀ f₁ P) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyWith.symm F) x = ↑F (unitInterval.symm x.fst, x.snd)

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 : ContinuousMap.HomotopyWith f₀ f₁ P) : ContinuousMap.HomotopyWith f₁ f₀ P

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

@[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 : ContinuousMap.HomotopyWith f₀ f₁ P) : ContinuousMap.HomotopyWith.symm (ContinuousMap.HomotopyWith.symm F) = F

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 : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) : ContinuousMap.HomotopyWith f₀ 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].

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 : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyWith.trans F G) x = if h : ↑x.fst ≤ 1 / 2 then ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ unitInterval) }, x.snd) else ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ unitInterval) }, x.snd)

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 : ContinuousMap.HomotopyWith f₀ f₁ P) (G : ContinuousMap.HomotopyWith f₁ f₂ P) : ContinuousMap.HomotopyWith.symm (ContinuousMap.HomotopyWith.trans F G) = ContinuousMap.HomotopyWith.trans (ContinuousMap.HomotopyWith.symm G) (ContinuousMap.HomotopyWith.symm F)

@[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 : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyWith.cast F h₀ h₁) a = ↑F a

@[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 : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyWith.cast F 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 : ContinuousMap.HomotopyWith f₀ f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.HomotopyWith g₀ g₁ P

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

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) : 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.

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) : ContinuousMap.HomotopicWith f 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 : ContinuousMap.HomotopicWith f g P) : ContinuousMap.HomotopicWith g 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₀ : ContinuousMap.HomotopicWith f g P) (h₁ : ContinuousMap.HomotopicWith g h P) : ContinuousMap.HomotopicWith f h P

@[inline, reducible]

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.

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 : ContinuousMap.HomotopyRel f₀ 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 : ContinuousMap.HomotopyRel f₀ 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 : ContinuousMap.HomotopyRel f₀ f₁ S) {x : X} (hx : x ∈ S) : ↑f₀ x = ↑f₁ x

@[simp]

theorem ContinuousMap.HomotopyRel.refl_toFun {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.refl f S) x = ↑f x.snd

@[simp]

theorem ContinuousMap.HomotopyRel.refl_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.refl f S) x = ↑f x.snd

def ContinuousMap.HomotopyRel.refl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : Set X) : ContinuousMap.HomotopyRel f 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.

@[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 : ContinuousMap.HomotopyRel f₀ f₁ S) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.symm F) x = ↑F (unitInterval.symm x.fst, x.snd)

@[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 : ContinuousMap.HomotopyRel f₀ f₁ S) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.symm F) x = ↑F (unitInterval.symm x.fst, x.snd)

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 : ContinuousMap.HomotopyRel f₀ f₁ S) : ContinuousMap.HomotopyRel f₁ f₀ S

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

@[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 : ContinuousMap.HomotopyRel f₀ f₁ S) : ContinuousMap.HomotopyRel.symm (ContinuousMap.HomotopyRel.symm F) = F

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 : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) : ContinuousMap.HomotopyRel f₀ 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].

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 : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) (x : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.trans F G) x = if h : ↑x.fst ≤ 1 / 2 then ↑F ({ val := 2 * ↑x.fst, property := (_ : 2 * ↑x.fst ∈ unitInterval) }, x.snd) else ↑G ({ val := 2 * ↑x.fst - 1, property := (_ : 2 * ↑x.fst - 1 ∈ unitInterval) }, x.snd)

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 : ContinuousMap.HomotopyRel f₀ f₁ S) (G : ContinuousMap.HomotopyRel f₁ f₂ S) : ContinuousMap.HomotopyRel.symm (ContinuousMap.HomotopyRel.trans F G) = ContinuousMap.HomotopyRel.trans (ContinuousMap.HomotopyRel.symm G) (ContinuousMap.HomotopyRel.symm F)

@[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 : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.cast F h₀ h₁) a = ↑F a

@[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 : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (a : ↑unitInterval × X) : ↑(ContinuousMap.HomotopyRel.cast F 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 : ContinuousMap.HomotopyRel f₀ f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) : ContinuousMap.HomotopyRel g₀ g₁ S

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

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

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.

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 : ContinuousMap.HomotopicRel f₀ f₁ S) : ContinuousMap.Homotopic f₀ 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)) : ContinuousMap.HomotopicRel f 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 : ContinuousMap.HomotopicRel f g S) : ContinuousMap.HomotopicRel g 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₀ : ContinuousMap.HomotopicRel f g S) (h₁ : ContinuousMap.HomotopicRel g h S) : ContinuousMap.HomotopicRel f h S

theorem ContinuousMap.HomotopicRel.equivalence {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {S : Set X} : Equivalence fun f g => ContinuousMap.HomotopicRel f 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)} : ContinuousMap.HomotopicRel f₀ f₁ ∅ ↔ ContinuousMap.Homotopic f₀ f₁