English
The evaluation of the concatenated path γ.trans γ' at t is given by the same piecewise formula as trans_apply, expressed with t as an element of the unit interval.
Русский
Значение пути γ.trans γ' в точке t задаётся той же кусочной формулой, что и в trans_apply, с t∈I.
LaTeX
$$$(\gamma.trans\gamma')(t) = \begin{cases} \gamma(2t), & t\le 1/2 \\ \gamma'(2t-1), & \text{else} \end{cases}$$$
Lean4
@[simp]
theorem trans_symm (γ : Path x y) (γ' : Path y z) : (γ.trans γ').symm = γ'.symm.trans γ.symm :=
by
ext t
simp only [trans_apply, symm_apply, Function.comp_apply]
split_ifs with h h₁ h₂ <;> rw [coe_symm_eq] at h
· have ht : (t : ℝ) = 1 / 2 := by linarith
norm_num [ht]
· refine congr_arg _ (Subtype.ext ?_)
norm_num [sub_sub_eq_add_sub, mul_sub]
· refine congr_arg _ (Subtype.ext ?_)
simp only [coe_symm_eq]
ring
· exfalso
linarith
