map — Mathlib

English

The image of a path under a continuous map f is the path γ.map' restricted to the image of f.

Русский

Образ пути под непрерывным отображением f есть путь γ.map', полученный посредством f.

LaTeX

$$$\gamma.map'\{f: X \to Y\} (h: ContinuousOn f (range γ))$$$

Lean4

/-- Image of a path from `x` to `y` by a continuous map -/
def map (γ : Path x y) {f : X → Y} (h : Continuous f) : Path (f x) (f y) :=
  γ.map' h.continuousOn

Похожие утверждения