English
Let γ be a path from x to y in a space X. For any points x′, y′ with x′ = x and y′ = y, the path γ.cast hx hy from x′ to y′ is simply γ reinterpreted as a path with endpoints x′ and y′; in particular, its underlying trajectory is the same as γ. Consequently, γ.cast hx hy yields a path from x′ to y′ with the same image as γ, and if hx and hy are refl, then γ.cast rfl rfl = γ.
Русский
Пусть γ — путь из x в y в некотором топологическом пространстве X. Для любых точек x′, y′ такие, что x′ = x и y′ = y, путь γ.cast hx hy является тем же самым путём γ, но интерпретированным как путь from x′ к y′; по своей сути трасса γ не меняется. Следовательно, γ.cast hx hy задаёт путь из x′ в y′ с той же изображённой кривой как γ; и если hx, hy равны равенствам, то γ.cast rfl rfl = γ.
LaTeX
$$$\gamma\ cast\ x'\;y'\;hx\;hy: Path(x',y')\quad\text{where}\quad (\gamma.cast hx hy)(t)=\gamma(t)\quad(\forall t\in I).$$$
Lean4
/-- Casting a path from `x` to `y` to a path from `x'` to `y'` when `x' = x` and `y' = y` -/
def cast (γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : Path x' y'
where
toFun := γ
continuous_toFun := γ.continuous
source' := by simp [hx]
target' := by simp [hy]
