English
If F: f0 ~ f1 and G: g0 ~ g1 are Homotopies, then F.prodMap G is a Homotopy between f0.prodMap g0 and f1.prodMap g1; the homotopy is given by (F p, G p).
Русский
Если F: f0 ~ f1 и G: g0 ~ g1 — гомотопии, тогда F.prodMap G — гомотопия между f0.prodMap g0 и f1.prodMap g1; гомотопия задаётся как (F p, G p).
LaTeX
$$$$ F : f_0 \sim f_1 , \ G : g_0 \sim g_1 \Rightarrow F.prodMap G : (f_0.prodMap g_0) \sim (f_1.prodMap g_1) $$$$
Lean4
/-- Let `F` be a homotopy between `f₀ : C(X, Y)` and `f₁ : C(X, Y)`. Let `G` be a homotopy between
`g₀ : C(Z, Z')` and `g₁ : C(Z, Z')`. Then `F.prodMap G` is the homotopy between `f₀.prodMap g₀` and
`f₁.prodMap g₁` that sends `(t, x, z)` to `(F (t, x), G (t, z))`. -/
def prodMap {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(Z, Z')} (F : Homotopy f₀ f₁) (G : Homotopy g₀ g₁) :
Homotopy (f₀.prodMap g₀) (f₁.prodMap g₁) :=
.prodMk (F.compContinuousMap .fst) (G.compContinuousMap .snd)
