map — Mathlib

English

If h : p.Homotopic q and f : C(X,Y), then h.map f : p.map f ⟶ q.map f is a Homotopy.

Русский

Если h : p.Homotopic q и f : C(X,Y), то h.map f является гомотопией между p.map f и q.map f.

LaTeX

$$$\text{If } h: p.Homotopic q\text{ and } f,\; (p.map f.continuous).Homotopic (q.map f.continuous)$$$

Lean4

nonrec theorem map {p q : Path x₀ x₁} (h : p.Homotopic q) (f : C(X, Y)) :
    Homotopic (p.map f.continuous) (q.map f.continuous) :=
  h.map fun F => F.map f

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