English
If p is a path and f is a suitable reparametrization of the interval, then there is a homotopy from p to p.reparam f.
Русский
Если p — путь и f подходит как перестановка параметра, существует гомотопия от p к p.reparam f.
LaTeX
$$$\forall p:\, Path x_0 x_1,\; f:\, I \to I,\; (\text{Continuous } f) \Rightarrow p.Homotopy (p.reparam f)$$$
Lean4
/-- Suppose `p` is a path, then we have a homotopy from `p` to `p.reparam f` by the convexity of `I`.
-/
def reparam (p : Path x₀ x₁) (f : I → I) (hf : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
Homotopy p (p.reparam f hf hf₀ hf₁)
where
toFun
x :=
p
⟨σ x.1 * x.2 + x.1 * f x.2,
show (σ x.1 : ℝ) • (x.2 : ℝ) + (x.1 : ℝ) • (f x.2 : ℝ) ∈ I from
convex_Icc _ _ x.2.2 (f x.2).2 (by unit_interval) (by unit_interval) (by simp)⟩
map_zero_left x := by norm_num
map_one_left x := by norm_num
prop' t x
hx := by
rcases hx with hx | hx
· rw [hx]
simp [hf₀]
· rw [Set.mem_singleton_iff] at hx
rw [hx]
simp [hf₁]
continuous_toFun := by fun_prop
