Theorems · Definition · combinatorics

Prefunctor.IsCovering.casesOn

{U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} →
      [inst_1 : Quiver V] →
        {φ : U ⥤q V} →
          {motive : φ.IsCovering → Sort u_3} →
            (t : φ.IsCovering) →
              ((star_bijective : ∀ (u : U), Function.Bijective (φ.star u)) →
                  (costar_bijective : ∀ (u : U), Function.Bijective (φ.costar u)) → motive ⋯) →
                motive t

Defined in

Mathlib.Combinatorics.Quiver.Covering

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

QuiverQuiver