truncate_range — Mathlib

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]

Похожие утверждения