English
Let γ be a path in a topological space X. Then the uncurried map (t0, t1, s) ↦ γ.truncate t0 t1 s is continuous; i.e., γ.truncate extends to a continuous function of the three parameters t0, t1, and s.
Русский
Пусть γ — траектория в топологическом пространстве X. Тогда развёрнутая по трём аргументам функция (t0, t1, s) ↦ γ.truncate t0 t1 s непрерывна; то есть γ.truncate образует непрерывную семейство путей в зависимости от трёх параметров t0, t1 и s.
LaTeX
$$$ F: \mathbb{R} \times \mathbb{R} \times I \to X, \quad F(t_0,t_1,s) = \gamma.truncate\, t_0\, t_1\, s, \quad F \text{ is continuous}. $$$
Lean4
/-- For a path `γ`, `γ.truncate` gives a "continuous family of paths", by which we mean
the uncurried function which maps `(t₀, t₁, s)` to `γ.truncate t₀ t₁ s` is continuous. -/
@[continuity]
theorem truncate_continuous_family {a b : X} (γ : Path a b) :
Continuous (fun x => γ.truncate x.1 x.2.1 x.2.2 : ℝ × ℝ × I → X) :=
γ.continuous_extend.comp
(((continuous_subtype_val.comp (continuous_snd.comp continuous_snd)).max continuous_fst).min
(continuous_fst.comp continuous_snd))
