Theorems · Definition · order theory

GradeMinOrder.casesOn

{𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        {motive : GradeMinOrder 𝕆 α → Sort u} →
          (t : GradeMinOrder 𝕆 α) →
            ([toGradeOrder : GradeOrder 𝕆 α] →
                (isMin_grade : ∀ ⦃a : α⦄, IsMin a → IsMin (GradeOrder.grade a)) →
                  motive { toGradeOrder := toGradeOrder, isMin_grade := isMin_grade }) →
              motive t

Defined in

Mathlib.Order.Grade

Cited by

0 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

PreorderPreorder