English
If F : p.Homotopy q and f : C(X,Y) is continuous, then F.map f is a Homotopy between p.map f and q.map f.
Русский
Если F : p.Homotopy q и f : C(X,Y) непрерывна, то F.map f — гомотопия между p.map f и q.map f.
LaTeX
$$$\text{If } F : p.Homotopy q\text{ and } f : C(X,Y),\; (p.map f.continuous).Homotopy (q.map f.continuous)$$$
Lean4
/-- Given `F : Homotopy p q`, and `f : C(X, Y)`, we can define a homotopy from `p.map f.continuous` to
`q.map f.continuous`.
-/
@[simps]
def map {p q : Path x₀ x₁} (F : p.Homotopy q) (f : C(X, Y)) : Homotopy (p.map f.continuous) (q.map f.continuous)
where
toFun := f ∘ F
map_zero_left := by simp
map_one_left := by simp
prop' t x
hx := by
rcases hx with hx | hx
· simp [hx]
· rw [Set.mem_singleton_iff] at hx
simp [hx]
