English
If for every i the spaces X_i are homotopy equivalent to Y_i, then the function spaces ∀i X_i and ∀i Y_i are homotopy equivalent.
Русский
Если для каждого i пространства X_i гомотопически эквивалентно Y_i, то пространства функций ∀i X_i и ∀i Y_i гомотопически эквивалентны.
LaTeX
$$$\bigl(\forall i, X_i \simeq_h Y_i\bigr) \Rightarrow (\forall i, X_i) \simeq_h (\forall i, Y_i)$$$
Lean4
/-- If `X` is homotopy equivalent to `Y` and `Z` is homotopy equivalent to `Z'`, then `X × Z` is
homotopy equivalent to `Z × Z'`. -/
def prodCongr (h₁ : X ≃ₕ Y) (h₂ : Z ≃ₕ Z') : (X × Z) ≃ₕ (Y × Z')
where
toFun := h₁.toFun.prodMap h₂.toFun
invFun := h₁.invFun.prodMap h₂.invFun
left_inv := h₁.left_inv.prodMap h₂.left_inv
right_inv := h₁.right_inv.prodMap h₂.right_inv
