This module provides typeclass instances and lemmas about order-related typeclasses.

instance Std.instIrreflOfAsymm {α : Sort u_1} (r : α → α → Prop) [Asymm r] : Irrefl r

instance Std.instReflOfTotal {α : Sort u_1} {r : α → α → Prop} [Total r] : Refl r

instance Std.Total.asymm_of_total_not {α : Sort u_1} {r : α → α → Prop} [i : Total fun (x1 x2 : α) => ¬r x1 x2] : Asymm r

theorem Std.Asymm.total_not {α : Sort u_1} {r : α → α → Prop} [i : Asymm r] : Total fun (x1 x2 : α) => ¬r x1 x2

instance Std.instAntisymmLeOfIsPartialOrder {α : Type u} [LE α] [IsPartialOrder α] : Antisymm fun (x1 x2 : α) => x1 ≤ x2

instance Std.instTransLeOfIsPreorder {α : Type u} [LE α] [IsPreorder α] : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• Std.instTransLeOfIsPreorder = { trans := ⋯ }

instance Std.instReflLeOfIsPreorder {α : Type u} [LE α] [IsPreorder α] : Refl fun (x1 x2 : α) => x1 ≤ x2

instance Std.instTotalLeOfIsLinearPreorder {α : Type u} [LE α] [IsLinearPreorder α] : Total fun (x1 x2 : α) => x1 ≤ x2

theorem Std.le_refl {α : Type u} [LE α] [Refl fun (x1 x2 : α) => x1 ≤ x2] (a : α) : a ≤ a

theorem Std.le_antisymm {α : Type u} [LE α] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] {a b : α} (hab : a ≤ b) (hba : b ≤ a) : a = b

theorem Std.le_trans {α : Type u} [LE α] [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c

theorem Std.le_total {α : Type u} [LE α] [Total fun (x1 x2 : α) => x1 ≤ x2] {a b : α} : a ≤ b ∨ b ≤ a

instance Std.instReflLeOfIsPreorder_1 {α : Type u} [LE α] [IsPreorder α] : Refl fun (x1 x2 : α) => x1 ≤ x2

instance Std.instTransLeOfIsPreorder_1 {α : Type u} [LE α] [IsPreorder α] : Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• Std.instTransLeOfIsPreorder_1 = { trans := ⋯ }

instance Std.instTotalLeOfIsLinearPreorder_1 {α : Type u} [LE α] [IsLinearPreorder α] : Total fun (x1 x2 : α) => x1 ≤ x2

instance Std.instAntisymmLeOfIsPartialOrder_1 {α : Type u} [LE α] [IsPartialOrder α] : Antisymm fun (x1 x2 : α) => x1 ≤ x2

theorem Std.lt_iff_le_and_not_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem Std.not_lt {α : Type u} [LT α] [LE α] [Total fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderLT α] {a b : α} : ¬a < b ↔ b ≤ a

theorem Std.not_gt_of_lt {α : Type u} [LT α] [i : Asymm fun (x1 x2 : α) => x1 < x2] {a b : α} (h : a < b) : ¬b < a

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

instance Std.instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α] [IsPreorder α] [LawfulOrderLT α] : Irrefl fun (x1 x2 : α) => x1 < x2

instance Std.instTransLtOfLeOfLawfulOrderLT {α : Type u} [LT α] [LE α] [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderLT α] : Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2

Equations

• Std.instTransLtOfLeOfLawfulOrderLT = { trans := ⋯ }

instance Std.instAntisymmNotLtOfLawfulOrderLTOfTotalOfLe {α : Type u} {x✝ : LT α} [LE α] [LawfulOrderLT α] [Total fun (x1 x2 : α) => x1 ≤ x2] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] : Antisymm fun (x1 x2 : α) => ¬x1 < x2

instance Std.instTransNotLtOfLawfulOrderLTOfTotalOfLe {α : Type u} {x✝ : LT α} [LE α] [LawfulOrderLT α] [Total fun (x1 x2 : α) => x1 ≤ x2] [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] : Trans (fun (x1 x2 : α) => ¬x1 < x2) (fun (x1 x2 : α) => ¬x1 < x2) fun (x1 x2 : α) => ¬x1 < x2

Equations

• Std.instTransNotLtOfLawfulOrderLTOfTotalOfLe = { trans := ⋯ }

instance Std.instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {x✝ : LT α} [LE α] [LawfulOrderLT α] [Total fun (x1 x2 : α) => x1 ≤ x2] : Total fun (x1 x2 : α) => ¬x1 < x2

theorem Std.lt_of_le_of_lt {α : Type u} [LE α] [LT α] [Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderLT α] {a b c : α} (hab : a ≤ b) (hbc : b < c) : a < c

theorem Std.lt_of_le_of_ne {α : Type u} [LE α] [LT α] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderLT α] {a b : α} (hle : a ≤ b) (hne : a ≠ b) : a < b

def Classical.Order.instLT {α : Type u} [LE α] : LT α

Equations

• Classical.Order.instLT = { lt := fun (a b : α) => a ≤ b ∧ ¬b ≤ a }

instance Classical.Order.instLawfulOrderLT {α : Type u} [LE α] : Std.LawfulOrderLT α

theorem Std.min_self {α : Type u} [Min α] [IdempotentOp min] {a : α} : min a a = a

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

theorem Std.min_le_left {α : Type u} [Min α] [LE α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderInf α] {a b : α} : min a b ≤ a

theorem Std.min_le_right {α : Type u} [Min α] [LE α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderInf α] {a b : α} : min a b ≤ b

theorem Std.min_le {α : Type u} [Min α] [LE α] [IsPreorder α] [LawfulOrderMin α] {a b c : α} : min a b ≤ c ↔ a ≤ c ∨ b ≤ c

theorem Std.min_eq_or {α : Type u} [Min α] [MinEqOr α] {a b : α} : min a b = a ∨ min a b = b

instance Std.instMinEqOrOfIsLinearOrderOfLawfulOrderInf {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderInf α] : MinEqOr α

theorem Std.IsLinearOrder.of_refl_of_antisymm_of_lawfulOrderMin {α : Type u} [LE α] [LE α] [Min α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderMin α] : IsLinearOrder α

If a Min α instance satisfies typical properties in terms of a reflexive and antisymmetric LE α instance, then the LE α instance represents a linear order.

instance Std.instIdempotentOpMinOfMinEqOr {α : Type u} [Min α] [MinEqOr α] : IdempotentOp min

instance Std.instAssociativeMinOfIsLinearOrderOfLawfulOrderMin {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderMin α] : Associative min

theorem Std.max_self {α : Type u} [Max α] [IdempotentOp max] {a : α} : max a a = a

theorem Std.max_le_iff {α : Type u} [Max α] [LE α] [LawfulOrderSup α] {a b c : α} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem Std.left_le_max {α : Type u} [Max α] [LE α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderSup α] {a b : α} : a ≤ max a b

theorem Std.right_le_max {α : Type u} [Max α] [LE α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderSup α] {a b : α} : b ≤ max a b

theorem Std.le_max {α : Type u} [Max α] [LE α] [IsPreorder α] [LawfulOrderMax α] {a b c : α} : a ≤ max b c ↔ a ≤ b ∨ a ≤ c

theorem Std.max_eq_or {α : Type u} [Max α] [MaxEqOr α] {a b : α} : max a b = a ∨ max a b = b

instance Std.instMaxEqOrOfIsLinearOrderOfLawfulOrderSup {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderSup α] : MaxEqOr α

theorem Std.IsLinearOrder.of_refl_of_antisymm_of_lawfulOrderMax {α : Type u} [LE α] [Max α] [Refl fun (x1 x2 : α) => x1 ≤ x2] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] [LawfulOrderMax α] : IsLinearOrder α

If a Max α instance satisfies typical properties in terms of a reflexive and antisymmetric LE α instance, then the LE α instance represents a linear order.

instance Std.instMaxSubtypeOfMaxEqOr {α : Type u} [Max α] [MaxEqOr α] {P : α → Prop} : Max (Subtype P)

Equations

• Std.instMaxSubtypeOfMaxEqOr = { max := fun (a b : Subtype P) => ⟨max a.val b.val, ⋯⟩ }

instance Std.instIdempotentOpMaxOfMaxEqOr {α : Type u} [Max α] [MaxEqOr α] : IdempotentOp max

instance Std.instAssociativeMaxOfIsLinearOrderOfLawfulOrderMax {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderMax α] : Associative max