English
Concatenation of two paths γ from x to y and γ' from y to z yields a path from x to z, putting the first on [0,1/2] and the second on [1/2,1].
Русский
Сцепление двух путей γ: x→y и γ': y→z даёт путь x→z, первый держится на [0,1/2], второй — на [1/2,1].
LaTeX
$$@(γ.trans γ'). toFun is defined by toFun(t) = if t ≤ 1/2 then γ.extend(2t) else γ'.extend(2t-1)$$
Lean4
theorem trans_apply (γ : Path x y) (γ' : Path y z) (t : I) :
(γ.trans γ') t =
if h : (t : ℝ) ≤ 1 / 2 then γ ⟨2 * t, (mul_pos_mem_iff zero_lt_two).2 ⟨t.2.1, h⟩⟩
else γ' ⟨2 * t - 1, two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, t.2.2⟩⟩ :=
show ite _ _ _ = _ by split_ifs <;> rw [extend_extends]
