This module provides utilities for the creation of order-related typeclass instances.

@[inline]

def Min.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Min α

Creates a Min α instance from LE α and DecidableLE α so that min a b is either a or b, preferring a over b when in doubt.

Has a LawfulOrderLeftLeaningMin α instance.

Equations

• Min.leftLeaningOfLE α = { min := fun (a b : α) => if a ≤ b then a else b }

@[inline]

def Max.leftLeaningOfLE (α : Type u) [LE α] [DecidableLE α] : Max α

Creates a Max α instance from LE α and DecidableLE α so that max a b is either a or b, preferring a over b when in doubt.

Has a LawfulOrderLeftLeaningMax α instance.

Equations

• Max.leftLeaningOfLE α = { max := fun (a b : α) => if b ≤ a then a else b }

theorem Std.IsPreorder.of_le {α : Type u} [LE α] (le_refl : Refl fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_trans : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) : IsPreorder α

If an LE α instance is reflexive and transitive, then it represents a preorder.

theorem Std.IsLinearPreorder.of_le {α : Type u} [LE α] (le_trans : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_total : Total fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) : IsLinearPreorder α

If an LE α instance is transitive and total, then it represents a linear preorder.

theorem Std.IsPartialOrder.of_le {α : Type u} [LE α] (le_refl : Refl fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_antisymm : Antisymm fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_trans : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) : IsPartialOrder α

If an LE α is reflexive, antisymmetric and transitive, then it represents a partial order.

theorem Std.IsLinearOrder.of_le {α : Type u} [LE α] (le_antisymm : Antisymm fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_trans : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) (le_total : Total fun (x1 x2 : α) => x1 ≤ x2 := by exact inferInstance) : IsLinearOrder α

If an LE α instance is antisymmetric, transitive and total, then it represents a linear order.

theorem Std.LawfulOrderLT.of_le {α : Type u} [LT α] [LE α] (lt_iff : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) : LawfulOrderLT α

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

theorem Std.LawfulOrderBEq.of_le {α : Type u} [BEq α] [LE α] (beq_iff : ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a) : LawfulOrderBEq α

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

theorem Std.LawfulOrderInf.of_le {α : Type u} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) : LawfulOrderInf α

This lemma characterizes in terms of LE α when a Min α instance "behaves like an infimum operator".

theorem Std.LawfulOrderMin.of_le_min_iff {α : Type u} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c := by exact LawfulOrderInf.le_min_iff) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b := by exact MinEqOr.min_eq_or) : LawfulOrderMin α

Returns a LawfulOrderMin α instance given certain properties.

This lemma derives a LawfulOrderMin α instance from two properties involving LE α and Min α instances.

The produced instance entails LawfulOrderInf α and MinEqOr α.

theorem Std.LawfulOrderMin.of_min_le {α : Type u} [Min α] [LE α] [i : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] (min_le_left : ∀ (a b : α), min a b ≤ a) (min_le_right : ∀ (a b : α), min a b ≤ b) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b := by exact MinEqOr.min_eq_or) : LawfulOrderMin α

Returns a LawfulOrderMin α instance given that max a b returns either a or b and that it is less than or equal to both of them. The ≤ relation needs to be transitive.

The produced instance entails LawfulOrderInf α and MinEqOr α.

def Std.LawfulOrderSup.of_le {α : Type u} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max a b ≤ c ↔ a ≤ c ∧ b ≤ c) : LawfulOrderSup α

This lemma characterizes in terms of LE α when a Max α instance "behaves like a supremum operator".

Equations

• ⋯ = ⋯

def Std.LawfulOrderMax.of_max_le_iff {α : Type u} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max a b ≤ c ↔ a ≤ c ∧ b ≤ c := by exact LawfulOrderInf.le_min_iff) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b := by exact MaxEqOr.max_eq_or) : LawfulOrderMax α

Returns a LawfulOrderMax α instance given certain properties.

This lemma derives a LawfulOrderMax α instance from two properties involving LE α and Max α instances.

The produced instance entails LawfulOrderSup α and MaxEqOr α.

Equations

• ⋯ = ⋯

theorem Std.LawfulOrderMax.of_le_max {α : Type u} [Max α] [LE α] [i : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] (left_le_max : ∀ (a b : α), a ≤ max a b) (right_le_max : ∀ (a b : α), b ≤ max a b) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b := by exact MaxEqOr.max_eq_or) : LawfulOrderMax α

Returns a LawfulOrderMax α instance given that max a b returns either a or b and that it is larger than or equal to both of them. The ≤ relation needs to be transitive.

The produced instance entails LawfulOrderSup α and MaxEqOr α.

@[inline]

def LE.ofLT (α : Type u) [LT α] : LE α

Creates a total LE α instance from an LT α instance.

This only makes sense for asymmetric LT α instances (see Std.Asymm).

Equations

• LE.ofLT α = { le := fun (a b : α) => ¬b < a }

instance Std.LawfulOrderLT.of_lt {α : Type u} [LT α] [i : Asymm fun (x1 x2 : α) => x1 < x2] : LawfulOrderLT α

The LE α instance obtained from an asymmetric LT α instance is compatible with said LT α instance.

theorem Std.IsLinearPreorder.of_lt {α : Type u} [LT α] (lt_asymm : Asymm fun (x1 x2 : α) => x1 < x2 := by exact inferInstance) (not_lt_trans : Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2 := by exact inferInstance) : IsLinearPreorder α

If an LT α instance is asymmetric and its negation is transitive, then LE.ofLT α represents a linear preorder.

theorem Std.IsLinearOrder.of_lt {α : Type u} [LT α] (lt_asymm : Asymm fun (x1 x2 : α) => x1 < x2 := by exact inferInstance) (not_lt_trans : Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2 := by exact inferInstance) (not_lt_antisymm : Antisymm fun (x1 x2 : α) => ¬x1 < x2 := by exact inferInstance) : IsLinearOrder α

If an LT α instance is asymmetric and its negation is transitive and antisymmetric, then LE.ofLT α represents a linear order.

theorem Std.LawfulOrderInf.of_lt {α : Type u} [Min α] [LT α] (min_lt_iff : ∀ (a b c : α), min b c < a ↔ b < a ∨ c < a) : LawfulOrderInf α

This lemma characterizes in terms of LT α when a Min α instance "behaves like an infimum operator" with respect to LE.ofLT α.

theorem Std.LawfulOrderMin.of_lt {α : Type u} [Min α] [LT α] (min_lt_iff : ∀ (a b c : α), min b c < a ↔ b < a ∨ c < a) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) : LawfulOrderMin α

Derives a LawfulOrderMin α instance for LE.ofLT from two properties involving LT α and Min α instances.

The produced instance entails LawfulOrderInf α and MinEqOr α.

def Std.LawfulOrderSup.of_lt {α : Type u} [Max α] [LT α] (lt_max_iff : ∀ (a b c : α), c < max a b ↔ c < a ∨ c < b) : LawfulOrderSup α

This lemma characterizes in terms of LT α when a Max α instance "behaves like an supremum operator" with respect to LE.ofLT α.

Equations

• ⋯ = ⋯

def Std.LawfulOrderMax.of_lt {α : Type u} [Max α] [LT α] (lt_max_iff : ∀ (a b c : α), c < max a b ↔ c < a ∨ c < b) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) : LawfulOrderMax α

Derives a LawfulOrderMax α instance for LE.ofLT from two properties involving LT α and Max α instances.

The produced instance entails LawfulOrderSup α and MaxEqOr α.

Equations

• ⋯ = ⋯