English
Let {Y_i} be a family of spaces and {f0_i}, {f1_i} maps X → Y_i for each i. If for every i, f0_i ~ f1_i via F_i, then the pointwise family π f0 ~ π f1 is homotopic.
Русский
Пусть {Y_i} — семейство пространств, а для каждого i имеются отображения f0_i, f1_i: X → Y_i; если для каждого i существует гомотопия f0_i ~ f1_i через F_i, то π f0 ~ π f1 гомотопично.
LaTeX
$$$$ (\forall i, f_{0,i} \sim f_{1,i}) \Rightarrow \pi f_0 \sim \pi f_1 $$$$
Lean4
/-- Given a family of homotopies `F i` between `f₀ i : C(X, Y i)` and `f₁ i : C(X, Y i)`, returns a
homotopy between `ContinuousMap.pi f₀` and `ContinuousMap.pi f₁`. -/
protected def pi {Y : ι → Type*} [∀ i, TopologicalSpace (Y i)] {f₀ f₁ : ∀ i, C(X, Y i)}
(F : ∀ i, Homotopy (f₀ i) (f₁ i)) : Homotopy (.pi f₀) (.pi f₁)
where
toContinuousMap := .pi fun i ↦ F i
map_zero_left x := funext fun i ↦ (F i).map_zero_left x
map_one_left x := funext fun i ↦ (F i).map_one_left x
