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

structure ContinuousMap.Homotopy {X : Type u} {Y : Type v} [] [] (f₀ : C(X, Y)) (f₁ : C(X, Y)) extends :
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 : Y
• 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} [] [] {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} [] [] {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)} [] [] (F : Type u_5) (f₀ : outParam C(X, Y)) (f₁ : outParam C(X, Y)) [FunLike F () Y] extends :

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),
• 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)} [] [] {F : Type u_5} {f₀ : outParam C(X, Y)} {f₁ : outParam C(X, Y)} [FunLike F () Y] [self : ] (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)} [] [] {F : Type u_5} {f₀ : outParam C(X, Y)} {f₁ : outParam C(X, Y)} [FunLike F () Y] [self : ] (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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
FunLike (f₀.Homotopy f₁) () 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} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : f₀.Homotopy f₁} {G : f₀.Homotopy f₁} (h : ∀ (x : ), F x = G x) :
F = G
def ContinuousMap.Homotopy.Simps.apply {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) :
Y

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} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (t : ) (x : X) :
(F.curry t) x = F (t, x)
def ContinuousMap.Homotopy.extend {X : Type u} {Y : Type v} [] [] {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
• F.extend =
Instances For
theorem ContinuousMap.Homotopy.extend_apply_of_le_zero {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (t : ) (x : X) :
(F.extend t) x = F (t, x)
@[simp]
theorem ContinuousMap.Homotopy.extend_apply_of_mem_I {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {t : } (ht : ) (x : X) :
(F.extend t) x = F (t, ht, x)
theorem ContinuousMap.Homotopy.congr_fun {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {F : f₀.Homotopy f₁} {G : f₀.Homotopy f₁} (h : F = G) (x : ) :
F x = G x
theorem ContinuousMap.Homotopy.congr_arg {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) {x : } {y : } (h : x = y) :
F x = F y
@[simp]
theorem ContinuousMap.Homotopy.refl_apply {X : Type u} {Y : Type v} [] [] (f : C(X, Y)) (x : ) :
= f x.2
def ContinuousMap.Homotopy.refl {X : Type u} {Y : Type v} [] [] (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
• = { toFun := fun (x : ) => f x.2, continuous_toFun := , map_zero_left := , map_one_left := }
Instances For
instance ContinuousMap.Homotopy.instInhabitedId {X : Type u} [] :
Inhabited (().Homotopy ())
Equations
• ContinuousMap.Homotopy.instInhabitedId = { default := }
@[simp]
theorem ContinuousMap.Homotopy.symm_apply {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.Homotopy f₁) (x : ) :
F.symm x = F (, x.2)
def ContinuousMap.Homotopy.symm {X : Type u} {Y : Type v} [] [] {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
• F.symm = { toFun := fun (x : ) => F (, x.2), continuous_toFun := , map_zero_left := , map_one_left := }
Instances For
@[simp]
theorem ContinuousMap.Homotopy.symm_symm {X : Type u} {Y : Type v} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
Function.Bijective ContinuousMap.Homotopy.symm
def ContinuousMap.Homotopy.trans {X : Type u} {Y : Type v} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {f₂ : C(X, Y)} (F : f₀.Homotopy f₁) (G : f₁.Homotopy f₂) (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} [] [] {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} [] [] {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 : ) :
(F.cast h₀ h₁) a = F a
def ContinuousMap.Homotopy.cast {X : Type u} {Y : Type v} [] [] {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} [] [] [] {g₀ : C(Y, Z)} {g₁ : C(Y, Z)} (G : g₀.Homotopy g₁) (f : C(X, Y)) :
∀ (a : ), (G.compContinuousMap f) a = G (a.1, f a.2)
def ContinuousMap.Homotopy.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {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
• G.compContinuousMap f = { toContinuousMap := G.comp (.prodMap f), map_zero_left := , map_one_left := }
Instances For
@[simp]
theorem ContinuousMap.Homotopy.hcomp_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {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 : ) :
(F.hcomp G) x = G (x.1, F x)
def ContinuousMap.Homotopy.hcomp {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {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 : ) => 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} [] [] [] {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} [] [] [] [] {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} [] {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)) :
().Homotopy ()

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
• = { toContinuousMap := ContinuousMap.pi fun (i : ι) => (F i), map_zero_left := , map_one_left := }
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)) :
().Homotopy ()

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} [] [] (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} [] [] (f : C(X, Y)) :
f.Homotopic f
theorem ContinuousMap.Homotopic.symm {X : Type u} {Y : Type v} [] [] ⦃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} [] [] ⦃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} [] [] [] {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} [] [] :
Equivalence ContinuousMap.Homotopic
theorem ContinuousMap.Homotopic.prodMk {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {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} [] [] [] [] {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} [] {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)) :
().Homotopic ()

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

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} [] [] (f₀ : C(X, Y)) (f₁ : C(X, Y)) (P : C(X, Y)Prop) extends :
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 : Y
• 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 : ), 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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (self : f₀.HomotopyWith f₁ P) (t : ) :
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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} :
FunLike (f₀.HomotopyWith f₁ P) () 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} [] [] {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} [] [] {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} [] [] {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 : ), F x = G x) :
F = G
def ContinuousMap.HomotopyWith.Simps.apply {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) :
Y

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} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {P : C(X, Y)Prop} (F : f₀.HomotopyWith f₁ P) (t : ) :
P (F.curry t)
theorem ContinuousMap.HomotopyWith.extendProp {X : Type u} {Y : Type v} [] [] {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} [] [] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) (x : ) :
x = f x.2
@[simp]
theorem ContinuousMap.HomotopyWith.refl_toFun {X : Type u} {Y : Type v} [] [] {P : C(X, Y)Prop} (f : C(X, Y)) (hf : P f) (x : ) :
x = f x.2
def ContinuousMap.HomotopyWith.refl {X : Type u} {Y : Type v} [] [] {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
• = { toHomotopy := , prop' := }
Instances For
instance ContinuousMap.HomotopyWith.instInhabitedIdTrue {X : Type u} [] :
Inhabited (().HomotopyWith () fun (x : C(X, X)) => True)
Equations
• ContinuousMap.HomotopyWith.instInhabitedIdTrue = { default := }
@[simp]
theorem ContinuousMap.HomotopyWith.symm_toFun {X : Type u} {Y : Type v} [] [] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (x : ) :
F.symm x = F (, x.2)
@[simp]
theorem ContinuousMap.HomotopyWith.symm_apply {X : Type u} {Y : Type v} [] [] {P : C(X, Y)Prop} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyWith f₁ P) (x : ) :
F.symm x = F (, x.2)
def ContinuousMap.HomotopyWith.symm {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {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 : ) :
(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} [] [] {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} [] [] {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 : ) :
(F.cast h₀ h₁) a = F a
@[simp]
theorem ContinuousMap.HomotopyWith.cast_toFun {X : Type u} {Y : Type v} [] [] {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 : ) :
(F.cast h₀ h₁) a = F a
def ContinuousMap.HomotopyWith.cast {X : Type u} {Y : Type v} [] [] {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} [] [] (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} [] [] {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} [] [] {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} [] [] {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} [] [] (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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (t : ) {x : X} (hx : x S) :
F (t, x) = f₀ x
theorem ContinuousMap.HomotopyRel.eq_snd {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (t : ) {x : X} (hx : x S) :
F (t, x) = f₁ x
theorem ContinuousMap.HomotopyRel.fst_eq_snd {X : Type u} {Y : Type v} [] [] {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]
theorem ContinuousMap.HomotopyRel.refl_apply {X : Type u} {Y : Type v} [] [] (f : C(X, Y)) (S : Set X) (x : ) :
= f x.2
@[simp]
theorem ContinuousMap.HomotopyRel.refl_toFun {X : Type u} {Y : Type v} [] [] (f : C(X, Y)) (S : Set X) (x : ) :
= f x.2
def ContinuousMap.HomotopyRel.refl {X : Type u} {Y : Type v} [] [] (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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (x : ) :
F.symm x = F (, x.2)
@[simp]
theorem ContinuousMap.HomotopyRel.symm_apply {X : Type u} {Y : Type v} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} {S : Set X} (F : f₀.HomotopyRel f₁ S) (x : ) :
F.symm x = F (, x.2)
def ContinuousMap.HomotopyRel.symm {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {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 : ) :
(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} [] [] {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} [] [] {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 : ) :
(F.cast h₀ h₁) a = F a
@[simp]
theorem ContinuousMap.HomotopyRel.cast_apply {X : Type u} {Y : Type v} [] [] {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 : ) :
(F.cast h₀ h₁) a = F a
def ContinuousMap.HomotopyRel.cast {X : Type u} {Y : Type v} [] [] {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} [] [] [] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) (x : ) :
(F.compContinuousMap g) x = g (F x)
@[simp]
theorem ContinuousMap.HomotopyRel.compContinuousMap_apply {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {S : Set X} {f₀ : C(X, Y)} {f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) (x : ) :
(F.compContinuousMap g) x = g (F x)
def ContinuousMap.HomotopyRel.compContinuousMap {X : Type u} {Y : Type v} {Z : Type w} [] [] [] {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
• F.compContinuousMap g = { toHomotopy := F.hcomp , prop' := }
Instances For
def ContinuousMap.HomotopicRel {X : Type u} {Y : Type v} [] [] (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} [] [] {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} [] [] {S : Set X} (f : C(X, Y)) :
f.HomotopicRel f S
theorem ContinuousMap.HomotopicRel.symm {X : Type u} {Y : Type v} [] [] {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} [] [] {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} [] [] {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} [] [] {f₀ : C(X, Y)} {f₁ : C(X, Y)} :
f₀.HomotopicRel f₁ f₀.Homotopic f₁