Theorems · Definition · order theory

ConditionallyCompletePartialOrder.noConfusion

{P : Sort u} →
  {α : Type u_3} →
    {t : ConditionallyCompletePartialOrder α} →
      {α' : Type u_3} →
        {t' : ConditionallyCompletePartialOrder α'} →
          α = α' → t ≍ t' → ConditionallyCompletePartialOrder.noConfusionType P t t'

Defined in

Mathlib.Order.ConditionallyCompletePartialOrder.Defs

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms