map_trans — Mathlib

English

The map of a concatenated path equals the concatenation of the mapped paths.

Русский

Образ сцепленного пути равен сцеплению образованных путей.

LaTeX

$$$(\gamma.trans \gamma').map h = (\gamma.map h).trans (\gamma'.map h)$$$

Lean4

@[simp]
theorem map_trans (γ : Path x y) (γ' : Path y z) {f : X → Y} (h : Continuous f) :
    (γ.trans γ').map h = (γ.map h).trans (γ'.map h) := by
  ext t
  rw [trans_apply, map_coe, Function.comp_apply, trans_apply]
  split_ifs <;> rfl

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