English
The path obtained from γ by applying a map f is γ.map' with toFun = f ∘ γ and continuity on the image range of γ.
Русский
Путь, полученный из γ применением отображения f, имеет toFun = f ∘ γ и непрерывность на образе γ.
LaTeX
$$$\gamma.map' {f: X \to Y} (h: ContinuousOn f (range \gamma)) \;:\; \text{Path}(f x)(f y)$ with toFun = f \circ \gamma$$
Lean4
/-- Image of a path from `x` to `y` by a map which is continuous on the path. -/
def map' (γ : Path x y) {f : X → Y} (h : ContinuousOn f (range γ)) : Path (f x) (f y)
where
toFun := f ∘ γ
continuous_toFun := h.comp_continuous γ.continuous (fun x ↦ mem_range_self x)
source' := by simp
target' := by simp
