English
The image of a path-homotopy class under a continuous map f is obtained by applying f pointwise to the representative path, and this is compatible with the quotient.
Русский
Образ класса гомотопии пути через непрерывное отображение f получается применением f к представительному пути по точкам, и это согласуется с кванто-инверсией.
LaTeX
$$$\mathrm{mapFn} (P_0 : Path.Homotopic.Quotient x_0 x_1)\; (f : C(X,Y)) = \mathrm{Quotient.map} (\lambda q: q.map f.continuous) (\lambda _ _ h => Path.Homotopic.map h f) P_0$$$
Lean4
/-- The image of a path homotopy class `P₀` under a map `f`.
This is `Path.map` descended to the quotient. -/
def mapFn (P₀ : Path.Homotopic.Quotient x₀ x₁) (f : C(X, Y)) : Path.Homotopic.Quotient (f x₀) (f x₁) :=
Quotient.map (fun q : Path x₀ x₁ => q.map f.continuous) (fun _ _ h => Path.Homotopic.map h f) P₀
