English
The relative product of a family of homotopies between f_i and g_i, parameterized by i, yields a single homotopy Rel between pi f and pi g, respecting S.
Русский
Относительное произведение семейства гомотопий между f_i и g_i образует единую гомотопию Rel между pi f и pi g, соответствующую S.
LaTeX
$$$\mathrm{pi} (\{f_i\}, \{g_i\}, S) : \mathrm{HomotopyRel}(\mathrm{pi} f, \mathrm{pi} g)\; S$$$
Lean4
/-- The relative product of homotopies `F` and `G`,
where `F` takes `f₀` to `f₁` and `G` takes `g₀` to `g₁` -/
@[simps!]
def prod (F : HomotopyRel f₀ f₁ S) (G : HomotopyRel g₀ g₁ S) : HomotopyRel (prodMk f₀ g₀) (prodMk f₁ g₁) S
where
toHomotopy := Homotopy.prod F.toHomotopy G.toHomotopy
prop' t x hx := Prod.ext (F.prop' t x hx) (G.prop' t x hx)
