Theorems · Definition · combinatorics

Quiver.Path.casesOn

{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) →
            motive a Quiver.Path.nil →
              ({b c : V} → (a_2 : Quiver.Path a b) → (a_3 : b ⟶ c) → motive c (a_2.cons a_3)) → motive a_1 t

Defined in

Mathlib.Combinatorics.Quiver.Path

Cited by

12 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Quiver