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.compare_eq_of_lt_iff {α : Type u} [LE α] [LT α] [LawfulOrderLT α] [Ord α] [LawfulOrderOrd α] {a b : α} {o : Ordering} (h₁ : a < b ↔ o = Ordering.lt) (h₂ : b < a ↔ o = Ordering.gt) : compare a b = o

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 α

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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.

theorem 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_ite_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

@[deprecated Std.min_eq_ite_isLE_compare (since := "2026-07-21")]

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_ite_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

@[deprecated Std.max_eq_ite_isGE_compare (since := "2026-07-21")]

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

instance Std.instCommutativeMinOfLawfulOrderLeftLeaningMinOfIsLinearOrder {α : Type u_1} [LE α] [Min α] [LawfulOrderLeftLeaningMin α] [IsLinearOrder α] : Commutative min

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

instance Std.lawfulOrderOrd_compareOfLessAndEq {α : Type u} [LE α] [LT α] [Total fun (x1 x2 : α) => x1 ≤ x2] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] [DecidableLT α] [LawfulOrderLT α] [DecidableEq α] : LawfulOrderOrd α

theorem Std.lt_iff_of_strictMono {α : Type u_1} {β : Type u_2} [LT α] [Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Asymm fun (x1 x2 : β) => x1 < x2] {f : α → β} (hf : ∀ (x y : α), x < y → f x < f y) {x y : α} : f x < f y ↔ x < y

theorem Std.injective_of_strictMono {α : Type u_1} {β : Type u_2} [LT α] [Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Irrefl fun (x1 x2 : β) => x1 < x2] {f : α → β} (hf : ∀ (x y : α), x < y → f x < f y) : Function.Injective f

theorem Std.inj_of_strictMono {α : Type u_1} {β : Type u_2} [LT α] [Trichotomous fun (x1 x2 : α) => x1 < x2] [LT β] [Irrefl fun (x1 x2 : β) => x1 < x2] {f : α → β} (hf : ∀ (x y : α), x < y → f x < f y) {x y : α} : f x = f y ↔ x = y

@[instance_reducible]

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 α