English
If there is a relative homotopy from f0 to f1 and from f1 to f2 relative to S, then there is a relative homotopy from f0 to f2 relative to S obtained by pasting the two along the midpoint.
Русский
Если существует относительная гомотопия от f0 к f1 и от f1 к f2 относительно S, то существует относительная гомотопия от f0 к f2 относительно S, полученная склеиванием на середине.
LaTeX
$$$F:\mathrm{HomotopyRel}(f_0,f_1;S),\ G:\mathrm{HomotopyRel}(f_1,f_2;S) \implies F\!\trans\!G:\mathrm{HomotopyRel}(f_0,f_2;S).$$$
Lean4
/-- Given `HomotopyRel f₀ f₁ S` and `HomotopyRel f₁ f₂ S`, we can define a `HomotopyRel f₀ f₂ S`
by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
-/
def trans (F : HomotopyRel f₀ f₁ S) (G : HomotopyRel f₁ f₂ S) : HomotopyRel f₀ f₂ S
where
toHomotopy := F.toHomotopy.trans G.toHomotopy
prop' t x
hx := by
simp only [Homotopy.trans]
split_ifs
· simp [HomotopyWith.extendProp F (2 * t) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]
· simp [HomotopyWith.extendProp G (2 * t - 1) x hx, F.fst_eq_snd hx, G.fst_eq_snd hx]
