English
Given Homotopies F: f0→f1 and G: f1→f2, define a Homotopy from f0 to f2 by using F on the first half of the parameter interval and G on the second half, with appropriate reparametrization.
Русский
Задаем гомотопию f0→f2 путём использования F на первой половине параметрического отрезка и G на второй половине с соответствующей перераспределительностью.
LaTeX
$$$\text{trans}: (F: f_0 \to f_1) \to (G: f_1 \to f_2) \mapsto (f_0 \to f_2)$, заданная неравной формулой на пару (t, x).$$
Lean4
/-- 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]`.
-/
def trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) : Homotopy f₀ f₂
where
toFun x := if (x.1 : ℝ) ≤ 1 / 2 then F.extend (2 * x.1) x.2 else G.extend (2 * x.1 - 1) x.2
continuous_toFun :=
by
refine
continuous_if_le (by fun_prop) continuous_const (F.continuous.comp (by continuity)).continuousOn
(G.continuous.comp (by continuity)).continuousOn ?_
rintro x hx
norm_num [hx]
map_zero_left x := by norm_num
map_one_left x := by norm_num
