English
Let f0, f1, f2 be maps X → Y. If F is a homotopy from f0 to f1 and G is a homotopy from f1 to f2, then the concatenation F.trans G gives a homotopy from f0 to f2. On the unit interval, (F.trans G)(t, x) = F(2t, x) for t ≤ 1/2 and (F.trans G)(t, x) = G(2t − 1, x) for t ≥ 1/2.
Русский
Пусть f0, f1, f2 : X → Y. Пусть F — гомотопия от f0 к f1, и G — гомотопия от f1 к f2. Тогда конкатенация F.trans G задаёт гомотопию от f0 к f2. На интервале единицы (t ∈ [0,1]) (F.trans G)(t, x) равно F(2t, x) при t ≤ 1/2 и равно G(2t − 1, x) при t ≥ 1/2.
LaTeX
$$$ (F \text{ trans } G) : \mathrm{Homotopy}(f_0, f_2) $$$
Lean4
theorem trans_apply {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homotopy f₁ f₂) (x : I × X) :
(F.trans G) x =
if h : (x.1 : ℝ) ≤ 1 / 2 then F (⟨2 * x.1, (unitInterval.mul_pos_mem_iff zero_lt_two).2 ⟨x.1.2.1, h⟩⟩, x.2)
else G (⟨2 * x.1 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.1.2.2⟩⟩, x.2) :=
show ite _ _ _ = _ by
split_ifs <;>
· rw [extend, ContinuousMap.coe_IccExtend, Set.IccExtend_of_mem]
rfl
