Theorems · Definition · order theory

GradeMinOrder.liftRight

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

Lifts a graded order along a strictly monotone function.

Defined in

Mathlib.Order.Grade

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

PreorderPreorderPreorderGradeMinOrder