composePath_comp' — Mathlib

English

Let X, Y, Z be objects in a category C. If f is a path from X to Y and g is a path from Y to Z, then the path-level composition satisfies the same rule as ordinary morphism composition: composePath (f ≫ g) = composePath f ≫ composePath g.

Русский

Пусть X, Y, Z — объекты категории C. Пусть f — путь X→Y, g — путь Y→Z. Тогда конкатенация путей f и g соответствует обычной композиции морфизм: composePath (f ≫ g) = composePath f ≫ composePath g.

LaTeX

$$$\\operatorname{composePath}(f \\;\\overset{\\mathrm{≫}}{ } g) = \\operatorname{composePath}(f) \\;\\mathrm{≫} \\; \\operatorname{composePath}(g)$$$

Lean4

@[simp]
theorem composePath_comp' {X Y Z : Paths C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    composePath (f ≫ g) = composePath f ≫ composePath g :=
  composePath_comp f g

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