English
From a line map f: R → X, continuous on the unit interval I, with f(0) = x and f(1) = y, one obtains a path from x to y by restricting f to I and reparameterizing to the unit interval.
Русский
Из линейной карты f: R → X, непрерывной на единичном интервале I, с f(0)=x и f(1)=y, получается путь от x до y путём ограничения f к I и параметрирования заново к единичному интервалу.
LaTeX
$$$\mathrm{ofLine}\{f: \mathbb{R} \to X\}\; (hf: \text{ContinuousOn } f I)\; (h_0: f(0)=x) (h_1: f(1)=y)$ defines a Path x y by toFun = f \circ (\iota: I \to \mathbb{R})$ and the indicated continuity and endpoints.$$
Lean4
/-- The path obtained from a map defined on `ℝ` by restriction to the unit interval. -/
def ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y
where
toFun := f ∘ ((↑) : unitInterval → ℝ)
continuous_toFun := hf.comp_continuous continuous_subtype_val Subtype.prop
source' := h₀
target' := h₁
