Theorems · Definition · combinatorics

Quiver.Path.cons.elim

{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) →
            t.ctorIdx = 1 →
              ({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: 0 results in Mathlib
Foundations: Depth 9 from the axioms · uses no axioms
Assumes: Quiver

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
Quiverstatement and proof · cited by 405
Quiver.Pathstatement and proof · cited by 166
Quiver.Path.ctorIdxstatement and proof · cited by 3
Quiver.Path.ctorElimproof · cited by 0

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.