Mathlib Map

Theorems · Definition · category theory

Prefunctor.casesOn

{V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} →
      [inst_1 : Quiver W] →
        {motive : V ⥤q W → Sort u} →
          (t : V ⥤q W) →
            ((obj : V → W) → (map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)) → motive { obj := obj, map := map }) →
              motive t
Defined in
Mathlib.Combinatorics.Quiver.Prefunctor
Cited by
4 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
QuiverQuiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Prefunctor.ext · cited by 5Prefunctor.extCategoryTheory.Paths.lift_spec · cited by 1Paths.lift_specCategoryTheory.ReflPrefunctor.ext · cited by 1ReflPrefunctor.extPrefunctor.ext' · cited by 1Prefunctor.ext'Prefunctor.noConfusion · cited by 0Prefunctor.noConfusionPrefunctor.noConfusionType · cited by 0Prefunctor.noConfusionTypeQuiver.Hom · cited by 32603Quiver.HomQuiver · cited by 405QuiverPrefunctor · cited by 116PrefunctorPrefunctor.casesOnCITED BYCITES

Cites3

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
  • Prefunctorstatement and proof · cited by 116

Cited by6

Results whose statement or proof uses this declaration.