English
For any path γ and any t, truncating γ at t with both endpoints equal to t yields the extended path γ.extend t, up to a canonical reparametrization identified with the same end. In particular, γ.truncate t t coincides with the extended path γ.extend t under the natural identification.
Русский
Для любой траектории γ и любого t усечение γ по точке t с одинаковыми концами даёт расширенный путь γ.extend t, совпадающий с γ.truncate t t при естественном сопряжении.
LaTeX
$$$ \gamma.truncate(t,t) = \big( \mathrm{Path.refl}(\gamma.extend(t)) \big).cast (\text{by } \text{rw }[\min_self])\, (\gamma.extend(t)). $$$
Lean4
@[simp]
theorem truncate_self {a b : X} (γ : Path a b) (t : ℝ) :
γ.truncate t t = (Path.refl <| γ.extend t).cast (by rw [min_self]) rfl :=
by
ext x
by_cases hx : x ≤ t <;> simp [truncate]
