English
If F: f0 i ~ f1 i for each i and G: g0 j ~ g1 j for each j, then F.prodMap G yields a Homotopy between f0.prodMap g0 and f1.prodMap g1, acting pointwise by (F(t, x), G(t, z)).
Русский
Если для каждого i имеется F_i: f0 i ~ f1 i и для каждого j имеется G_j: g0 j ~ g1 j, то F.prodMap G задаёт гомотопию между f0.prodMap g0 и f1.prodMap g1, acting по точкам как (F(t, x), G(t, z)).
LaTeX
$$$$ F \prodMap G : (f_0.prodMap g_0) \sim (f_1.prodMap g_1) $$$$
Lean4
/-- If each `f₀ i : C(X, Y i)` is homotopic to `f₁ i : C(X, Y i)`, then `ContinuousMap.pi f₀` is
homotopic to `ContinuousMap.pi f₁`. -/
protected theorem pi {Y : ι → Type*} [∀ i, TopologicalSpace (Y i)] {f₀ f₁ : ∀ i, C(X, Y i)}
(F : ∀ i, Homotopic (f₀ i) (f₁ i)) : Homotopic (.pi f₀) (.pi f₁) :=
⟨.pi fun i ↦ (F i).some⟩
