English
Let F be a homotopy between f0 and f1 and G between g0 and g1. Then F.prodMk G provides a Homotopy between the products f0.prodMk g0 and f1.prodMk g1; the witness sends p to (F p, G p).
Русский
Пусть F — гомотопия между f0 и f1, и G — между g0 и g1. Тогда F.prodMk G задаёт гомотопию между произведениями f0.prodMk g0 и f1.prodMk g1; отображение p ↦ (F p, G p).
LaTeX
$$$$ F : f_0 \sim f_1 , \ G : g_0 \sim g_1 \Rightarrow F.prodMk G : (f_0.prodMk g_0) \sim (f_1.prodMk 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(X, Z)` and `g₁ : C(X, Z)`. Then `F.prodMk G` is the homotopy between `f₀.prodMk g₀` and
`f₁.prodMk g₁` that sends `p` to `(F p, G p)`. -/
nonrec def prodMk {f₀ f₁ : C(X, Y)} {g₀ g₁ : C(X, Z)} (F : Homotopy f₀ f₁) (G : Homotopy g₀ g₁) :
Homotopy (f₀.prodMk g₀) (f₁.prodMk g₁)
where
toContinuousMap := F.prodMk G
map_zero_left _ := Prod.ext (F.map_zero_left _) (G.map_zero_left _)
map_one_left _ := Prod.ext (F.map_one_left _) (G.map_one_left _)
