Theorems · Theorem · combinatorics

Quiver.Path.brecOn.eq

∀ {V : Type u} [inst : Quiver V] {a : V} {motive : (a_1 : V) → Quiver.Path a a_1 → Sort u_1} {a_1 : V}
  (t : Quiver.Path a a_1) (F_1 : (a_2 : V) → (t : Quiver.Path a a_2) → Quiver.Path.below t → motive a_2 t),
  Quiver.Path.brecOn t F_1 = F_1 a_1 t (Quiver.Path.brecOn.go t F_1).2

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

6 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Quiver