English
Two consecutive HomotopyWiths can be concatenated into a HomotopyWith f0 f2 P by placing one on [0,1/2] and the other on [1/2,1].
Русский
Две последовательные гомотопии можно соединить в одну gомотопию между f0 и f2, разместив одну на [0,1/2], другую на [1/2,1].
LaTeX
$$$\\text{trans}(F,G) : HomotopyWith(f_0,f_2,P)$$$
Lean4
/-- Given `HomotopyWith f₀ f₁ P` and `HomotopyWith f₁ f₂ P`, we can define a `HomotopyWith f₀ f₂ P`
by putting the first homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
-/
def trans {f₀ f₁ f₂ : C(X, Y)} (F : HomotopyWith f₀ f₁ P) (G : HomotopyWith f₁ f₂ P) : HomotopyWith f₀ f₂ P :=
{ F.toHomotopy.trans G.toHomotopy with
prop' := fun t => by
simp only [Homotopy.trans]
change P ⟨fun _ => ite ((t : ℝ) ≤ _) _ _, _⟩
split_ifs
· exact F.extendProp _
· exact G.extendProp _ }
