Theorems · Definition · order theory

GradeOrder.liftRight

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

Lifts a graded order along a strictly monotone function.

Defined in

Mathlib.Order.Grade

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

PreorderPreorderPreorderGradeOrder