Theorems · Definition · order theory

LinearOrder.liftWithOrd

{α : Type u_2} →
  {β : Type u_3} →
    [inst : LinearOrder β] →
      [inst_1 : Max α] →
        [inst_2 : Min α] →
          [inst_3 : Ord α] →
            (f : α → β) →
              Function.Injective f →
                (∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) →
                  (∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) →
                    (∀ (a b : α), compare a b = compare (f a) (f b)) → LinearOrder α

Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Max α] and [Min α] as arguments, then uses them for max and min fields. It also takes [Ord α] as an argument and uses them for compare fields. See LinearOrder.lift for a version that autogenerates compare fields, and LinearOrder.liftWithOrd' for one that auto-generates min and max fields. fields. See note [reducible non-instances].

Defined in

Mathlib.Order.Basic

Cited by

0 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext

Assumes

LinearOrderMaxMinOrd