Theorems · Definition · order theory

SuccAddOrder.noConfusion

{P : Sort u} →
  {α : Type u_1} →
    {inst : Preorder α} →
      {inst_1 : Add α} →
        {inst_2 : One α} →
          {t : SuccAddOrder α} →
            {α' : Type u_1} →
              {inst' : Preorder α'} →
                {inst'_1 : Add α'} →
                  {inst'_2 : One α'} →
                    {t' : SuccAddOrder α'} →
                      α = α' →
                        inst ≍ inst' →
                          inst_1 ≍ inst'_1 → inst_2 ≍ inst'_2 → t ≍ t' → SuccAddOrder.noConfusionType P t t'

Defined in

Mathlib.Algebra.Order.SuccPred

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms