English
The value of F.trans G at a point x is obtained by applying F on the first half and G on the second half, with the time rescaled appropriately.
Русский
Значение F.trans G в точке x определяется применением F к первому половинному отрезку времени и G ко второму, с соответствующим масштабированием времени.
LaTeX
$$$\forall F : p_0.Homotopy p_1,\; G : p_1.Homotopy p_2,\; x : I \times I,\; (F.trans G)(x) = \begin{cases} F.eval(x.1) , & x.2 \le 1/2 \\ G.eval(x.1) , & \text{иначе} \end{cases}$$$
Lean4
theorem trans_apply (F : Homotopy p₀ p₁) (G : Homotopy p₁ p₂) (x : I × I) :
(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) :=
ContinuousMap.HomotopyRel.trans_apply _ _ _
