English
Given a homotopy H between f and g, the path traced by a fixed x ∈ X is t ↦ H(t,x), from f(x) to g(x).
Русский
При гомотопии H между f и g траектория для фиксированного x — это путь t ↦ H(t, x) от f(x) к g(x).
LaTeX
$$$\mathrm{evalAt}(H,x) : Path\,(f(x))\,(g(x))\;\text{ defined by }\; (\mathrm{toFun}\; t) = H(t,x),\; \mathrm{source'}=H(0,x),\; \mathrm{target'}=H(1,x)$$$
Lean4
/-- Given a homotopy `H : f ∼ g`, get the path traced by the point `x` as it moves from
`f x` to `g x`.
-/
def evalAt {X : Type*} {Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f g : C(X, Y)}
(H : ContinuousMap.Homotopy f g) (x : X) : Path (f x) (g x)
where
toFun t := H (t, x)
source' := H.apply_zero x
target' := H.apply_one x
