Theorems · Definition · order theory

GradeBoundedOrder.liftRight

{𝕆 : Type u_1} →
  {α : Type u_3} →
    {β : Type u_4} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [GradeBoundedOrder 𝕆 β] →
              (f : α → β) →
                StrictMono f →
                  (∀ (a b : α), a ⋖ b → f a ⋖ f b) →
                    (∀ (a : α), IsMin a → IsMin (f a)) → (∀ (a : α), IsMax a → IsMax (f a)) → GradeBoundedOrder 𝕆 α

Lifts a graded order along a strictly monotone function.

Defined in

Mathlib.Order.Grade

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

PreorderPreorderPreorderGradeBoundedOrder