Theorems · Theorem · combinatorics

Prefunctor.mapPath_comp

∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] (F : V ⥤q W) {a b : V} (p : Quiver.Path a b) {c : V}
  (q : Quiver.Path b c), F.mapPath (p.comp q) = (F.mapPath p).comp (F.mapPath q)

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

QuiverQuiver