map — Mathlib

English

If a path in F from x to y exists, then mapping the path by a continuous function yields a path in the image from f(x) to f(y).

Русский

Если существует путь в F от x к y, отображение по непрерывной функции образует путь в изображение от f(x) к f(y).

LaTeX

$$JoinedIn F x y → JoinedIn (Set.image f F) (f x) (f y)$$

Lean4

theorem map (h : JoinedIn F x y) {f : X → Y} (hf : Continuous f) : JoinedIn (f '' F) (f x) (f y) :=
  h.map_continuousOn hf.continuousOn

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