English
Let X be a topological space and γ a path from a to b in X. For any real numbers t0 and t1, there exists a path γ_truncate from γ.extend(min(t0,t1)) to γ.extend(t1) that follows γ on the time interval [t0,t1] and remains constant outside that interval. In particular, γ_truncate(s) = γ.extend(min(max(s, t0), t1)) for all s.
Русский
Пусть X — топологическое пространство и γ — путь от a до b в X. Для любых действительных t0, t1 существует путь γ_truncate от γ.extend(min(t0,t1)) до γ.extend t1, который следует за γ на времени [t0,t1] и вне этого интервала остается постоянным. В частности, для всех s выполняется γ_truncate(s) = γ.extend(min(max(s, t0), t1)).
LaTeX
$$$\\exists \\tau: Path(\\gamma.extend(\\min\\{t_0,t_1\\}), \\gamma.extend(t_1)) \\quad\\text{such that}\\quad \\forall s,\\ \\tau(s) = \\gamma.extend(\\min(\\max s\\ t_0)\\ t_1).$$$
Lean4
/-- `γ.truncate t₀ t₁` is the path which follows the path `γ` on the time interval `[t₀, t₁]`
and stays still otherwise. -/
def truncate {X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ) :
Path (γ.extend <| min t₀ t₁) (γ.extend t₁)
where
toFun s := γ.extend (min (max s t₀) t₁)
continuous_toFun := γ.continuous_extend.comp ((continuous_subtype_val.max continuous_const).min continuous_const)
source' := by
simp only [min_def, max_def']
split_ifs with h₁ h₂ h₃ h₄
· simp [γ.extend_of_le_zero h₁]
· congr
linarith
· have h₄ : t₁ ≤ 0 := le_of_lt (by simpa using h₂)
simp [γ.extend_of_le_zero h₄, γ.extend_of_le_zero h₁]
all_goals rfl
target' := by
simp only [min_def, max_def']
split_ifs with h₁ h₂ h₃
· simp [γ.extend_of_one_le h₂]
· rfl
· have h₄ : 1 ≤ t₀ := le_of_lt (by simpa using h₁)
simp [γ.extend_of_one_le h₄, γ.extend_of_one_le (h₄.trans h₃)]
· rfl
