Theorems · Definition · order theory

GradeMaxOrder.recOn

{𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        {motive : GradeMaxOrder 𝕆 α → Sort u} →
          (t : GradeMaxOrder 𝕆 α) →
            ([toGradeOrder : GradeOrder 𝕆 α] →
                (isMax_grade : ∀ ⦃a : α⦄, IsMax a → IsMax (GradeOrder.grade a)) →
                  motive { toGradeOrder := toGradeOrder, isMax_grade := isMax_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