English
The range of the truncated path is contained in the range of the original path: range(γ.truncate(t0,t1)) ⊆ range(γ).
Русский
Образ урезанного пути содержится в образе исходного пути: range(γ.truncate(t0,t1)) ⊆ range(γ).
LaTeX
$$$\mathrm{range}(\gamma.\mathrm{truncate}(t_0,t_1)) \subseteq \mathrm{range}(\gamma).$$$
Lean4
theorem truncate_range {a b : X} (γ : Path a b) {t₀ t₁ : ℝ} : range (γ.truncate t₀ t₁) ⊆ range γ :=
by
rw [← γ.extend_range]
simp only [range_subset_iff, SetCoe.forall]
intro x _hx
simp only [DFunLike.coe, Path.truncate, mem_range_self]