Theorems · Definition · order theory

GradeBoundedOrder.recOn

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