English
Two continuous maps f0, f1 : X → Y are homotopic if there exists a Homotopy f0 f1 connecting them.
Русский
Две непрерывные отображения f0, f1 : X → Y гомотопны, если существует гомотопия от f0 к f1.
LaTeX
$$$$ f_0 \sim f_1 \iff \exists H: X \times I \to Y, \; H \text{ continuous}, \; H(0,x)=f_0(x), \; H(1,x)=f_1(x) \ (\forall x\in X). $$$$
Lean4
/-- Given a family of homotopies `F i` between `f₀ i : C(X i, Y i)` and `f₁ i : C(X i, Y i)`,
returns a homotopy between `ContinuousMap.piMap f₀` and `ContinuousMap.piMap f₁`. -/
protected def piMap {X Y : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, TopologicalSpace (Y i)]
{f₀ f₁ : ∀ i, C(X i, Y i)} (F : ∀ i, Homotopy (f₀ i) (f₁ i)) : Homotopy (.piMap f₀) (.piMap f₁) :=
.pi fun i ↦ (F i).compContinuousMap <| .eval i
