English
If each Fi is a homotopy between fi and f'i, then the piMap of the family fi is homotopic to piMap of the family f'i.
Русский
Если для каждого i имеется гомотопия Fi между fi и f'i, то piMap семей fi гомотопично продолжается к piMap семей f'i.
LaTeX
$$$$ (\forall i, fi \sim f'i) \Rightarrow \mathrm{Homotopic}(\pi f, \pi f') $$$$
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 piMap {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)]
{f₀ f₁ : ∀ i, C(X i, Y i)} (F : ∀ i, Homotopic (f₀ i) (f₁ i)) : Homotopic (.piMap f₀) (.piMap f₁) :=
.pi fun i ↦ .comp (F i) (.refl <| .eval i)
