English
The explicit evaluation of the glued relative homotopy on a pair (t,x) is given by a piecewise expression using t's location relative to 1/2.
Русский
Явное вычисление склеенной относительной гомотопии на паре (t,x) выражено через кусочно-заданную формулу в зависимости от того, где находится t относительно 1/2.
LaTeX
$$$\text{For }(F,G):\mathrm{HomotopyRel}(f_0,f_1;S),\mathrm{HomotopyRel}(f_1,f_2;S),\; (F\trans G)(t,x)=\begin{cases}F(2t,⟨\cdot,\cdot\rangle),& t\le 1/2, \\ G(2t-1,⟨\cdot,\cdot\rangle),& t>1/2.\end{cases}$$$
Lean4
/-- Post-compose a homotopy relative to a set by a continuous function. -/
@[simps!]
def compContinuousMap {f₀ f₁ : C(X, Y)} (F : f₀.HomotopyRel f₁ S) (g : C(Y, Z)) : (g.comp f₀).HomotopyRel (g.comp f₁) S
where
toHomotopy := .comp (.refl g) F.toHomotopy
prop' t x hx := congr_arg g (F.prop t x hx)
