# mathlibdocumentation

topology.homotopy.basic

# Homotopy between functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Definitions #

• continuous_map.homotopy f₀ f₁ is the type of homotopies between f₀ and f₁.
• continuous_map.homotopy_with f₀ f₁ P is the type of homotopies between f₀ and f₁, where the intermediate maps satisfy the predicate P.
• continuous_map.homotopy_rel 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 : continuous_map.homotopy f₀ f₁, then F.symm : continuous_map.homotopy f₁ f₀.
• trans F G, which concatenates the homotopies F and G. For example, if F : continuous_map.homotopy f₀ f₁ and G : continuous_map.homotopy f₁ f₂, then F.trans G : continuous_map.homotopy f₀ f₂.

We also define the relations

• continuous_map.homotopic f₀ f₁ is defined to be nonempty (continuous_map.homotopy f₀ f₁)
• continuous_map.homotopic_with f₀ f₁ P is defined to be nonempty (continuous_map.homotopy_with f₀ f₁ P)
• continuous_map.homotopic_rel f₀ f₁ P is defined to be nonempty (continuous_map.homotopy_rel f₀ f₁ P)

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

## References #

structure continuous_map.homotopy {X : Type u} {Y : Type v} (f₀ f₁ : C(X, Y)) :
Type (max u v)

continuous_map.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*} [homotopy_like F f₀ f₁] (f : F).

When you extend this structure, make sure to extend continuous_map.homotopy_like.

Instances for continuous_map.homotopy
@[nolint, instance]
def continuous_map.homotopy_like.to_continuous_map_class {X : Type u} {Y : Type v} (F : Type u_2) (f₀ f₁ : out_param C(X, Y)) [self : f₁] :
Y
@[class]
structure continuous_map.homotopy_like {X : Type u} {Y : Type v} (F : Type u_2) (f₀ f₁ : out_param C(X, Y)) :
Type (max u u_2 v)
• coe : F Π (a : , (λ (_x : , Y) a
• coe_injective' :
• map_continuous : (f : F),
• map_zero_left : (f : F) (x : X), f (0, x) = f₀ x
• map_one_left : (f : F) (x : X), f (1, x) = f₁ x

continuous_map.homotopy_like F f₀ f₁ states that F is a type of homotopies between f₀ and f₁.

You should extend this class when you extend continuous_map.homotopy.

Instances of this typeclass
Instances of other typeclasses for continuous_map.homotopy_like
• continuous_map.homotopy_like.has_sizeof_inst
@[protected, instance]
def continuous_map.homotopy.continuous_map.homotopy_like {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} :
f₀ f₁
Equations
@[protected, instance]
def continuous_map.homotopy.has_coe_to_fun {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} :
has_coe_to_fun (f₀.homotopy f₁) (λ (_x : f₀.homotopy f₁), Y)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[ext]
theorem continuous_map.homotopy.ext {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {F G : f₀.homotopy f₁} (h : (x : , F x = G x) :
F = G
def continuous_map.homotopy.simps.apply {X : Type u} {Y : Type v} {f₀ 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
@[protected]
theorem continuous_map.homotopy.continuous {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) :

Deprecated. Use map_continuous instead.

@[simp]
theorem continuous_map.homotopy.apply_zero {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) (x : X) :
F (0, x) = f₀ x
@[simp]
theorem continuous_map.homotopy.apply_one {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) (x : X) :
F (1, x) = f₁ x
@[simp]
theorem continuous_map.homotopy.coe_to_continuous_map {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) :
def continuous_map.homotopy.curry {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) :

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

Equations
@[simp]
theorem continuous_map.homotopy.curry_apply {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) (t : unit_interval) (x : X) :
((F.curry) t) x = F (t, x)
noncomputable def continuous_map.homotopy.extend {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) :

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

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

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

Equations
@[simp]
theorem continuous_map.homotopy.refl_apply {X : Type u} {Y : Type v} (f : C(X, Y)) (x : unit_interval × X) :
= f x.snd
@[protected, instance]
Equations
def continuous_map.homotopy.symm {X : Type u} {Y : Type v} {f₀ 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
@[simp]
theorem continuous_map.homotopy.symm_apply {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) (x : unit_interval × X) :
(F.symm) x = F , x.snd)
@[simp]
theorem continuous_map.homotopy.symm_symm {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy f₁) :
F.symm.symm = F
noncomputable def continuous_map.homotopy.trans {X : Type u} {Y : Type v} {f₀ f₁ 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
theorem continuous_map.homotopy.trans_apply {X : Type u} {Y : Type v} {f₀ f₁ f₂ : C(X, Y)} (F : f₀.homotopy f₁) (G : f₁.homotopy f₂) (x : unit_interval × X) :
(F.trans G) x = dite ((x.fst) 1 / 2) (λ (h : (x.fst) 1 / 2), F (2 * (x.fst), _⟩, x.snd)) (λ (h : ¬(x.fst) 1 / 2), G (2 * (x.fst) - 1, _⟩, x.snd))
theorem continuous_map.homotopy.symm_trans {X : Type u} {Y : Type v} {f₀ f₁ f₂ : C(X, Y)} (F : f₀.homotopy f₁) (G : f₁.homotopy f₂) :
@[simp]
theorem continuous_map.homotopy.cast_apply {X : Type u} {Y : Type v} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy f₁) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (ᾰ : unit_interval × X) :
(F.cast h₀ h₁) = F ᾰ
def continuous_map.homotopy.cast {X : Type u} {Y : Type v} {f₀ f₁ g₀ 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
@[simp]
theorem continuous_map.homotopy.hcomp_apply {X : Type u} {Y : Type v} {Z : Type w} {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (F : f₀.homotopy f₁) (G : g₀.homotopy g₁) (x : unit_interval × X) :
(F.hcomp G) x = G (x.fst, F x)
def continuous_map.homotopy.hcomp {X : Type u} {Y : Type v} {Z : Type w} {f₀ f₁ : C(X, Y)} {g₀ 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
def continuous_map.homotopic {X : Type u} {Y : Type v} (f₀ 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₁.

Equations
@[refl]
theorem continuous_map.homotopic.refl {X : Type u} {Y : Type v} (f : C(X, Y)) :
@[symm]
theorem continuous_map.homotopic.symm {X : Type u} {Y : Type v} ⦃f g : C(X, Y) (h : f.homotopic g) :
@[trans]
theorem continuous_map.homotopic.trans {X : Type u} {Y : Type v} ⦃f g h : C(X, Y) (h₀ : f.homotopic g) (h₁ : g.homotopic h) :
theorem continuous_map.homotopic.hcomp {X : Type u} {Y : Type v} {Z : Type w} {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Y, Z)} (h₀ : f₀.homotopic f₁) (h₁ : g₀.homotopic g₁) :
(g₀.comp f₀).homotopic (g₁.comp f₁)
structure continuous_map.homotopy_with {X : Type u} {Y : Type v} (f₀ f₁ : C(X, Y)) (P : C(X, Y) Prop) :
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

Instances for continuous_map.homotopy_with
@[protected, instance]
def continuous_map.homotopy_with.has_coe_to_fun {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} :
has_coe_to_fun (f₀.homotopy_with f₁ P) (λ (_x : f₀.homotopy_with f₁ P), Y)
Equations
theorem continuous_map.homotopy_with.coe_fn_injective {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} :
@[ext]
theorem continuous_map.homotopy_with.ext {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} {F G : f₀.homotopy_with f₁ P} (h : (x : , F x = G x) :
F = G
def continuous_map.homotopy_with.simps.apply {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with 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
@[protected, continuity]
theorem continuous_map.homotopy_with.continuous {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) :
@[simp]
theorem continuous_map.homotopy_with.apply_zero {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) (x : X) :
F (0, x) = f₀ x
@[simp]
theorem continuous_map.homotopy_with.apply_one {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) (x : X) :
F (1, x) = f₁ x
@[simp]
theorem continuous_map.homotopy_with.coe_to_continuous_map {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) :
@[simp]
theorem continuous_map.homotopy_with.coe_to_homotopy {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) :
theorem continuous_map.homotopy_with.prop {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) (t : unit_interval) :
theorem continuous_map.homotopy_with.extend_prop {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {P : C(X, Y) Prop} (F : f₀.homotopy_with f₁ P) (t : ) :
def continuous_map.homotopy_with.refl {X : Type u} {Y : Type v} {P : C(X, Y) Prop} (f : C(X, Y)) (hf : P f) :
P

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

Equations
@[simp]
theorem continuous_map.homotopy_with.refl_apply {X : Type u} {Y : Type v} {P : C(X, Y) Prop} (f : C(X, Y)) (hf : P f) (x : unit_interval × X) :
= f x.snd
@[simp]
theorem continuous_map.homotopy_with.refl_to_homotopy {X : Type u} {Y : Type v} {P : C(X, Y) Prop} (f : C(X, Y)) (hf : P f) :
@[protected, instance]
Equations
@[simp]
theorem continuous_map.homotopy_with.symm_apply {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (x : unit_interval × X) :
(F.symm) x = F , x.snd)
def continuous_map.homotopy_with.symm {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) :
f₁.homotopy_with f₀ P

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

Equations
@[simp]
theorem continuous_map.homotopy_with.symm_to_homotopy {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) :
@[simp]
theorem continuous_map.homotopy_with.symm_symm {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) :
F.symm.symm = F
noncomputable def continuous_map.homotopy_with.trans {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ f₂ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (G : f₁.homotopy_with f₂ P) :
f₀.homotopy_with f₂ P

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

Equations
theorem continuous_map.homotopy_with.trans_apply {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ f₂ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (G : f₁.homotopy_with f₂ P) (x : unit_interval × X) :
(F.trans G) x = dite ((x.fst) 1 / 2) (λ (h : (x.fst) 1 / 2), F (2 * (x.fst), _⟩, x.snd)) (λ (h : ¬(x.fst) 1 / 2), G (2 * (x.fst) - 1, _⟩, x.snd))
theorem continuous_map.homotopy_with.symm_trans {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ f₂ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (G : f₁.homotopy_with f₂ P) :
def continuous_map.homotopy_with.cast {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
g₀.homotopy_with g₁ P

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

Equations
@[simp]
theorem continuous_map.homotopy_with.cast_to_homotopy {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
(F.cast h₀ h₁).to_homotopy = F.to_homotopy.cast h₀ h₁
@[simp]
theorem continuous_map.homotopy_with.cast_apply {X : Type u} {Y : Type v} {P : C(X, Y) Prop} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_with f₁ P) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (ᾰ : unit_interval × X) :
(F.cast h₀ h₁) = F ᾰ
def continuous_map.homotopic_with {X : Type u} {Y : Type v} (f₀ 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 homotopy_with f₀ f₁ P.

Equations
@[refl]
theorem continuous_map.homotopic_with.refl {X : Type u} {Y : Type v} {P : C(X, Y) Prop} (f : C(X, Y)) (hf : P f) :
P
@[symm]
theorem continuous_map.homotopic_with.symm {X : Type u} {Y : Type v} {P : C(X, Y) Prop} ⦃f g : C(X, Y) (h : P) :
P
@[trans]
theorem continuous_map.homotopic_with.trans {X : Type u} {Y : Type v} {P : C(X, Y) Prop} ⦃f g h : C(X, Y) (h₀ : P) (h₁ : P) :
P
@[reducible]
def continuous_map.homotopy_rel {X : Type u} {Y : Type v} (f₀ f₁ : C(X, Y)) (S : set X) :
Type (max u v)

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

theorem continuous_map.homotopy_rel.eq_fst {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (t : unit_interval) {x : X} (hx : x S) :
F (t, x) = f₀ x
theorem continuous_map.homotopy_rel.eq_snd {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (t : unit_interval) {x : X} (hx : x S) :
F (t, x) = f₁ x
theorem continuous_map.homotopy_rel.fst_eq_snd {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) {x : X} (hx : x S) :
f₀ x = f₁ x
@[simp]
theorem continuous_map.homotopy_rel.refl_to_homotopy {X : Type u} {Y : Type v} (f : C(X, Y)) (S : set X) :
@[simp]
theorem continuous_map.homotopy_rel.refl_apply {X : Type u} {Y : Type v} (f : C(X, Y)) (S : set X) (x : unit_interval × X) :
= f x.snd
def continuous_map.homotopy_rel.refl {X : Type u} {Y : Type v} (f : C(X, Y)) (S : set X) :

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

Equations
@[simp]
theorem continuous_map.homotopy_rel.symm_apply {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (x : unit_interval × X) :
(F.symm) x = F , x.snd)
def continuous_map.homotopy_rel.symm {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) :
f₁.homotopy_rel f₀ S

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

Equations
@[simp]
theorem continuous_map.homotopy_rel.symm_to_homotopy {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) :
@[simp]
theorem continuous_map.homotopy_rel.symm_symm {X : Type u} {Y : Type v} {f₀ f₁ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) :
F.symm.symm = F
noncomputable def continuous_map.homotopy_rel.trans {X : Type u} {Y : Type v} {f₀ f₁ f₂ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (G : f₁.homotopy_rel f₂ S) :
f₀.homotopy_rel f₂ S

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

Equations
theorem continuous_map.homotopy_rel.trans_apply {X : Type u} {Y : Type v} {f₀ f₁ f₂ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (G : f₁.homotopy_rel f₂ S) (x : unit_interval × X) :
(F.trans G) x = dite ((x.fst) 1 / 2) (λ (h : (x.fst) 1 / 2), F (2 * (x.fst), _⟩, x.snd)) (λ (h : ¬(x.fst) 1 / 2), G (2 * (x.fst) - 1, _⟩, x.snd))
theorem continuous_map.homotopy_rel.symm_trans {X : Type u} {Y : Type v} {f₀ f₁ f₂ : C(X, Y)} {S : set X} (F : f₀.homotopy_rel f₁ S) (G : f₁.homotopy_rel f₂ S) :
def continuous_map.homotopy_rel.cast {X : Type u} {Y : Type v} {S : set X} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_rel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
g₀.homotopy_rel g₁ S

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

Equations
@[simp]
theorem continuous_map.homotopy_rel.cast_apply {X : Type u} {Y : Type v} {S : set X} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_rel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) (ᾰ : unit_interval × X) :
(F.cast h₀ h₁) = F ᾰ
@[simp]
theorem continuous_map.homotopy_rel.cast_to_homotopy {X : Type u} {Y : Type v} {S : set X} {f₀ f₁ g₀ g₁ : C(X, Y)} (F : f₀.homotopy_rel f₁ S) (h₀ : f₀ = g₀) (h₁ : f₁ = g₁) :
(F.cast h₀ h₁).to_homotopy = F.to_homotopy.cast h₀ h₁
def continuous_map.homotopic_rel {X : Type u} {Y : Type v} (f₀ 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 homotopy_rel f₀ f₁ S.

Equations
@[refl]
theorem continuous_map.homotopic_rel.refl {X : Type u} {Y : Type v} {S : set X} (f : C(X, Y)) :
S
@[symm]
theorem continuous_map.homotopic_rel.symm {X : Type u} {Y : Type v} {S : set X} ⦃f g : C(X, Y) (h : S) :
S
@[trans]
theorem continuous_map.homotopic_rel.trans {X : Type u} {Y : Type v} {S : set X} ⦃f g h : C(X, Y) (h₀ : S) (h₁ : S) :
S
theorem continuous_map.homotopic_rel.equivalence {X : Type u} {Y : Type v} {S : set X} :
equivalence (λ (f g : C(X, Y)), S)