English
Suppose F : p0.Homotopy q0 and G : p1.Homotopy q1. Then hcomp(F,G) is a Homotopy from p0.trans p1 to q0.trans q1.
Русский
Пусть F : p0.Homotopy q0 и G : p1.Homotopy q1. Тогда hcomp(F,G) — гомотопия от p0.trans p1 к q0.trans q1.
LaTeX
$$$\forall F : p_0.Homotopy q_0,\; G : p_1.Homotopy q_1\; \rightarrow (p_0.trans p_1).Homotopy (q_0.trans q_1)$$$
Lean4
/-- Suppose `p₀` and `q₀` are paths from `x₀` to `x₁`, `p₁` and `q₁` are paths from `x₁` to `x₂`.
Furthermore, suppose `F : Homotopy p₀ q₀` and `G : Homotopy p₁ q₁`. Then we can define a homotopy
from `p₀.trans p₁` to `q₀.trans q₁`.
-/
def hcomp (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) : Homotopy (p₀.trans p₁) (q₀.trans q₁)
where
toFun x := if (x.2 : ℝ) ≤ 1 / 2 then (F.eval x.1).extend (2 * x.2) else (G.eval x.1).extend (2 * x.2 - 1)
continuous_toFun :=
continuous_if_le (continuous_induced_dom.comp continuous_snd) continuous_const
(F.toHomotopy.continuous.comp (by continuity)).continuousOn
(G.toHomotopy.continuous.comp (by continuity)).continuousOn fun x hx => by norm_num [hx]
map_zero_left x := by simp [Path.trans]
map_one_left x := by simp [Path.trans]
prop' x t
ht := by
rcases ht with ht | ht
· norm_num [ht]
· rw [Set.mem_singleton_iff] at ht
norm_num [ht]
