English
Let X be a topological space and γ a continuous path from a to b. For every t in the unit interval [0,1], the extension γ.extend evaluated at t equals γ(t); i.e., extending a path on [0,1] does not alter its values on that interval.
Русский
Пусть X — топологическое множество и γ — непрерывный путь от a до b. Для каждого t ∈ единичном отрезке [0,1] выполняется γ.extend(t) = γ(t); то есть продолжение пути на [0,1] не изменяет его значения на этом отрезке.
LaTeX
$$$\forall t \in [0,1],\; \gamma.extend(t) = \gamma(t).$$$
Lean4
theorem extend_extends' {a b : X} (γ : Path a b) (t : (Icc 0 1 : Set ℝ)) : γ.extend t = γ t :=
IccExtend_val _ γ t
