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

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 α

Returns a LawfulOrderLT α instance given certain properties.

If an OrderData α instance is compatible with an LE α instance, then this lemma derives a LawfulOrderLT α instance from a property relating the LE α and LT α instances.

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 {α : Type u} [Min α] [LE α] (le_min_iff : ∀ (a b c : α), a ≤ min b c ↔ a ≤ b ∧ a ≤ c) (min_eq_or : ∀ (a b : α), min a b = a ∨ min a b = b) : 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 α.

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_le {α : Type u} [Max α] [LE α] (max_le_iff : ∀ (a b c : α), max a b ≤ c ↔ a ≤ c ∧ b ≤ c) (max_eq_or : ∀ (a b : α), max a b = a ∨ max a b = b) : 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

• ⋯ = ⋯

def Std.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

• Std.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 OrderData.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 OrderData.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 OrderData.ofLT from two properties involving LT α and Max α instances.

The produced instance entails LawfulOrderSup α and MaxEqOr α.

Equations

• ⋯ = ⋯