mapPath_comp' — Mathlib

English

For a Prefunctor F : V ⥤q W and X ⟶ Y ⟶ Z in Paths V, the map of the composition equals the composition of maps: F.mapPath (f ≫ g) = (F.mapPath f) . map (F.mapPath g).

Русский

Для префункторa F: V ⥤q W и морфизмов f: X ⟶ Y и g: Y ⟶ Z в Paths V выполняется: F.mapPath (f ≫ g) = (F.mapPath f) . map (F.mapPath g).

LaTeX

$$$F.mapPath (f \;\!\!\; g) = (F.mapPath f) . (F.mapPath g)$$$

Lean4

@[simp]
theorem mapPath_comp' (F : V ⥤q W) {X Y Z : Paths V} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.mapPath (f ≫ g) = (F.mapPath f).comp (F.mapPath g) :=
  Prefunctor.mapPath_comp _ _ _

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