English
A simps-projection for piCongrRight exists; it sends a family of homotopy equivalences to the corresponding map on the product spaces.
Русский
Существуют projection-симпс для пи-конгруэнтности правой стороны; они отправляют семейство гомотопических эквивалентностей в соответствующее отображение на произведение.
LaTeX
$$$\text{piCongrRight}(h): (\forall i, X_i) \simeq_h (\forall i, Y_i)$$$
Lean4
/-- If `X i` is homotopy equivalent to `Y i` for each `i`, then the space of functions (a.k.a. the
indexed product) `∀ i, X i` is homotopy equivalent to `∀ i, Y i`. -/
def piCongrRight {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)]
(h : ∀ i, X i ≃ₕ Y i) : (∀ i, X i) ≃ₕ (∀ i, Y i)
where
toFun := .piMap fun i ↦ (h i).toFun
invFun := .piMap fun i ↦ (h i).invFun
left_inv := .piMap fun i ↦ (h i).left_inv
right_inv := .piMap fun i ↦ (h i).right_inv
