English
For a fixed path γ and a fixed real number t, the two-variable map (t1, s) ↦ γ.truncate t t1 s is continuous; i.e., γ.truncate t is a continuous family of paths parameterized by (t1, s).
Русский
Для заданной траектории γ и фиксированного числа t отображение (t1, s) ↦ γ.truncate t t1 s непрерывно, то есть γ.truncate t образует непрерывное семейство путей в зависимости от порождающих t1 и s.
LaTeX
$$$ G_t: \mathbb{R} \times I \to X, \quad G_t(t_1,s) = \gamma.truncate\ t\ t_1\ s, \quad G_t \text{ is continuous for every } t. $$$
Lean4
@[continuity]
theorem truncate_const_continuous_family {a b : X} (γ : Path a b) (t : ℝ) : Continuous ↿(γ.truncate t) :=
by
have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop
exact γ.truncate_continuous_family.comp key
