English
For a path γ and a suitable reparametrization f: I → I with f(0)=0 and f(1)=1, the image of γ.reparam f equals the image of γ; i.e., reparameterization does not change the trace of the path.
Русский
Для траектории γ и подходящего отображения переparametrизации f: I → I с f(0)=0, f(1)=1 образ γ.reparam f совпадает с образом γ; переparametrизация не меняет трассу пути.
LaTeX
$$$\operatorname{range}(\gamma.reparam(f, \cdots)) = \operatorname{range}(\gamma).$$$
Lean4
/-- Given a path `γ` and a function `f : I → I` where `f 0 = 0` and `f 1 = 1`, `γ.reparam f` is the
path defined by `γ ∘ f`.
-/
def reparam (γ : Path x y) (f : I → I) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) : Path x y
where
toFun := γ ∘ f
continuous_toFun := by fun_prop
source' := by simp [hf₀]
target' := by simp [hf₁]
