Theorems · Definition · combinatorics

Prefunctor.MapReverse.recOn

{U : Type u_1} →
  {V : Type u_2} →
    [inst : Quiver U] →
      [inst_1 : Quiver V] →
        [inst_2 : Quiver.HasReverse U] →
          [inst_3 : Quiver.HasReverse V] →
            {φ : U ⥤q V} →
              {motive : φ.MapReverse → Sort u_3} →
                (t : φ.MapReverse) →
                  ((map_reverse' : ∀ {u v : U} (e : u ⟶ v), φ.map (Quiver.reverse e) = Quiver.reverse (φ.map e)) →
                      motive ⋯) →
                    motive t

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiver.HasReverseQuiver.HasReverse