English
If t0 ≤ t1, the truncated path γ.truncate(t0,t1) is viewed as a path from γ.extend(t0) to γ.extend(t1).
Русский
Если t0 ≤ t1, урезанный путь γ.truncate(t0,t1) является путём от γ.extend(t0) до γ.extend(t1).
LaTeX
$$$\text{If } t_0 \le t_1:\; \gamma\,\text{truncate}(t_0,t_1): (\gamma.extend t_0) \to (\gamma.extend t_1).$$$
Lean4
/-- `γ.truncateOfLE t₀ t₁ h`, where `h : t₀ ≤ t₁` is `γ.truncate t₀ t₁`
casted as a path from `γ.extend t₀` to `γ.extend t₁`. -/
def truncateOfLE {X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} (h : t₀ ≤ t₁) :
Path (γ.extend t₀) (γ.extend t₁) :=
(γ.truncate t₀ t₁).cast (by rw [min_eq_left h]) rfl
