Theorems · Definition · combinatorics

Quiver.Path.brecOn.go

{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) →
            ((a_2 : V) → (t : Quiver.Path a a_2) → Quiver.Path.below t → motive a_2 t) →
              motive a_1 t ×' Quiver.Path.below t

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

7 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

Quiver