English
If F is a homotopy from f0 to f1 and G is a homotopy from g0 to g1, then their product defines a homotopy from f0.prodMk g0 to f1.prodMk g1.
Русский
Если F — гомотопия от f0 к f1 и G — от g0 к g1, то их произведение задаёт гомотопию от f0.prodMk g0 к f1.prodMk g1.
LaTeX
$$$\mathrm{prod}(F,G) : \mathrm{Homotopy}(f_0\,\text{prodMk}\, g_0, f_1\,\text{prodMk}\, g_1)$$$
Lean4
/-- The product of homotopies `F` and `G`,
where `F` takes `f₀` to `f₁` and `G` takes `g₀` to `g₁` -/
@[simps]
def prod (F : Homotopy f₀ f₁) (G : Homotopy g₀ g₁) : Homotopy (ContinuousMap.prodMk f₀ g₀) (ContinuousMap.prodMk f₁ g₁)
where
toFun t := (F t, G t)
map_zero_left x := by simp only [prod_eval, Homotopy.apply_zero]
map_one_left x := by simp only [prod_eval, Homotopy.apply_one]
