Theorems · Definition · combinatorics

Quiver.HasInvolutiveReverse.noConfusion

{P : Sort u} →
  {V : Type u_2} →
    {inst : Quiver V} →
      {t : Quiver.HasInvolutiveReverse V} →
        {V' : Type u_2} →
          {inst' : Quiver V'} →
            {t' : Quiver.HasInvolutiveReverse V'} →
              V = V' → inst ≍ inst' → t ≍ t' → Quiver.HasInvolutiveReverse.noConfusionType P t t'

Defined in

Mathlib.Combinatorics.Quiver.Symmetric

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms