Theorems · Theorem · combinatorics

Prefunctor.mapPath_comp_apply

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

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses propext

Assumes

QuiverQuiverQuiver