instance Std.instOrientedOrdOfLawfulOrderOrd {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α] : OrientedOrd α

instance Std.instTransOrdOfLawfulOrderOrdOfIsPreorder {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [IsPreorder α] : TransOrd α

instance Std.instLawfulBEqOrdOfLawfulOrderOrdOfLawfulOrderBEq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α] : LawfulBEqOrd α

instance Std.instLawfulEqOrdOfLawfulOrderOrdOfIsPartialOrder {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [IsPartialOrder α] : LawfulEqOrd α

instance Std.instTotalLeOfLawfulOrderOrd {α : Type u_1} [Ord α] [LE α] [LawfulOrderOrd α] : Total fun (x1 x2 : α) => x1 ≤ x2

instance Std.instLawfulEqOrdOfLawfulOrderOrdOfAntisymmLe {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] : LawfulEqOrd α

instance Std.instAntisymmLeOfLawfulOrderOrdOfLawfulEqOrd {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] [LawfulEqOrd α] : Antisymm fun (x1 x2 : α) => x1 ≤ x2

theorem Std.compare_eq_eq_iff_eq {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : compare a b = Ordering.eq ↔ a = b

theorem Std.IsLinearPreorder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α] [TransOrd α] : IsLinearPreorder α

theorem Std.IsLinearOrder.of_ord {α : Type u} [LE α] [Ord α] [LawfulOrderOrd α] [TransOrd α] [LawfulEqOrd α] : IsLinearOrder α

instance Std.LawfulOrderLT.of_ord (α : Type u) [Ord α] [LT α] [LE α] [LawfulOrderOrd α] (lt_iff_compare_eq_lt : ∀ (a b : α), a < b ↔ compare a b = Ordering.lt) : LawfulOrderLT α

This lemma derives a LawfulOrderLT α instance from a property involving an Ord α instance.

instance Std.LawfulOrderBEq.of_ord (α : Type u) [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] (beq_iff_compare_eq_eq : ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq) : LawfulOrderBEq α

This lemma derives a LawfulOrderBEq α instance from a property involving an Ord α instance.

instance Std.LawfulOrderInf.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α] (compare_min_isLE_iff : ∀ (a b c : α), (compare a (min b c)).isLE = true ↔ (compare a b).isLE = true ∧ (compare a c).isLE = true) : LawfulOrderInf α

This lemma derives a LawfulOrderInf α instance from a property involving an Ord α instance.

instance Std.LawfulOrderMin.of_ord (α : Type u) [Ord α] [Min α] [LE α] [LawfulOrderOrd α] (compare_min_isLE_iff : ∀ (a b c : α), (compare a (min b c)).isLE = true ↔ (compare a b).isLE = true ∧ (compare a c).isLE = true) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) : LawfulOrderMin α

This lemma derives a LawfulOrderMin α instance from a property involving an Ord α instance.

instance Std.LawfulOrderSup.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α] (compare_max_isLE_iff : ∀ (a b c : α), (compare (max a b) c).isLE = true ↔ (compare a c).isLE = true ∧ (compare b c).isLE = true) : LawfulOrderSup α

This lemma derives a LawfulOrderSup α instance from a property involving an Ord α instance.

instance Std.LawfulOrderMax.of_ord (α : Type u) [Ord α] [Max α] [LE α] [LawfulOrderOrd α] (compare_max_isLE_iff : ∀ (a b c : α), (compare (max a b) c).isLE = true ↔ (compare a c).isLE = true ∧ (compare b c).isLE = true) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) : LawfulOrderMax α

This lemma derives a LawfulOrderMax α instance from a property involving an Ord α instance.

theorem Std.min_eq_if_isLE_compare {α : Type u} [Ord α] [LE α] {x✝ : Min α} [LawfulOrderOrd α] [LawfulOrderLeftLeaningMin α] {a b : α} : min a b = if (compare a b).isLE = true then a else b

theorem Std.max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {x✝ : Max α} [LawfulOrderOrd α] [LawfulOrderLeftLeaningMax α] {a b : α} : max a b = if (compare a b).isGE = true then a else b

noncomputable def Classical.Order.instOrd {α : Type u} [LE α] : Ord α

Derives an Ord α instance from an LE α instance. Because all elements are comparable with compare, the resulting Ord α instance only makes sense if LE α is total.

Equations

• Classical.Order.instOrd = { compare := fun (a b : α) => if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt }

instance Classical.Order.instLawfulOrderOrd {α : Type u} [LE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : Std.LawfulOrderOrd α