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_antisymm_iff {α : Type u} [LE α] [Antisymm fun (x1 x2 : α) => x1 ≤ x2] [Refl fun (x1 x2 : α) => x1 ≤ x2] {a b : α} : a ≤ b ∧ 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

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

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

theorem Std.le_of_lt {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} (h : a < b) : a ≤ b

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_lt_of_le {α : 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.beq_iff_le_and_ge {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] {a b : α} : (a == b) = true ↔ a ≤ b ∧ b ≤ a

instance Std.instSymmEqBoolBeqTrueOfLawfulOrderBEq {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] : Symm fun (x1 x2 : α) => (x1 == x2) = true

instance Std.instEquivBEqOfLawfulOrderBEqOfIsPreorder {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] [IsPreorder α] : EquivBEq α

instance Std.instLawfulBEqOfLawfulOrderBEqOfIsPartialOrder {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] [IsPartialOrder α] : LawfulBEq α

noncomputable def Classical.Order.instBEq {α : Type u} [LE α] : BEq α

Equations

• Classical.Order.instBEq = { beq := fun (a b : α) => decide (a ≤ b ∧ b ≤ a) }

instance Classical.Order.instLawfulOrderBEq {α : Type u} [LE α] : Std.LawfulOrderBEq α

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.min_eq_if {α : Type u} [LE α] [DecidableLE α] {x✝ : Min α} [LawfulOrderLeftLeaningMin α] {a b : α} : min a b = if a ≤ b then a else b

theorem Std.max_eq_if {α : Type u} [LE α] [DecidableLE α] {x✝ : Max α} [LawfulOrderLeftLeaningMax α] {a b : α} : max a b = if b ≤ a then a else b

instance Std.instLawfulOrderLeftLeaningMinOfIsLinearOrderOfLawfulOrderInf {α : Type u} [LE α] [Min α] [IsLinearOrder α] [LawfulOrderInf α] : LawfulOrderLeftLeaningMin α

theorem Std.LawfulOrderLeftLeaningMin.of_eq {α : Type u} [LE α] [Min α] [DecidableLE α] (min_eq : ∀ (a b : α), min a b = if a ≤ b then a else b) : LawfulOrderLeftLeaningMin α

instance Std.instLawfulOrderLeftLeaningMin {α : Type u_1} [LE α] [DecidableLE α] : LawfulOrderLeftLeaningMin α

instance Std.instMinEqOrOfLawfulOrderLeftLeaningMin {α : Type u} [LE α] [Min α] [LawfulOrderLeftLeaningMin α] : MinEqOr α

instance Std.instLawfulOrderMinOfIsLinearPreorderOfLawfulOrderLeftLeaningMin {α : Type u} [LE α] [Min α] [IsLinearPreorder α] [LawfulOrderLeftLeaningMin α] : LawfulOrderMin α

noncomputable def Classical.Order.instMin {α : Type u} [LE α] : Min α

Equations

• Classical.Order.instMin = Min.leftLeaningOfLE α

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

instance Std.instLawfulOrderLeftLeaningMaxOfIsLinearOrderOfLawfulOrderSup {α : Type u} [LE α] [Max α] [IsLinearOrder α] [LawfulOrderSup α] : LawfulOrderLeftLeaningMax α

theorem Std.LawfulOrderLeftLeaningMax.of_eq {α : Type u} [LE α] [Max α] [DecidableLE α] (min_eq : ∀ (a b : α), max a b = if b ≤ a then a else b) : LawfulOrderLeftLeaningMax α

instance Std.instLawfulOrderLeftLeaningMax {α : Type u_1} [LE α] [DecidableLE α] : LawfulOrderLeftLeaningMax α

instance Std.instMaxEqOrOfLawfulOrderLeftLeaningMax {α : Type u} [LE α] [Max α] [LawfulOrderLeftLeaningMax α] : MaxEqOr α

instance Std.instLawfulOrderMaxOfIsLinearPreorderOfLawfulOrderLeftLeaningMax {α : Type u} [LE α] [Max α] [IsLinearPreorder α] [LawfulOrderLeftLeaningMax α] : LawfulOrderMax α

noncomputable def Classical.Order.instMax {α : Type u} [LE α] : Max α

Equations

• Classical.Order.instMax = Max.leftLeaningOfLE α