Theorems · Theorem · combinatorics

Quiver.Push.lift_comp

∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [inst_1 : Quiver W'] (φ : V ⥤q W')
  (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)), Quiver.Push.of σ ⋙q Quiver.Push.lift σ φ τ h = φ

Defined in

Mathlib.Combinatorics.Quiver.Push

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses propext, Quot.sound

Assumes

QuiverQuiver