Init.Data.Order.Lemmas

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

source

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

Irrefl r

source

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

Refl r

source

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

Antisymm r

source

instance Std.instTrichotomousOfTotal {α : Sort u_1} (r : α → α → Prop) [Total r] :

Trichotomous r

source

theorem Std.Trichotomous.rel_or_eq_or_rel_swap {α : Sort u_1} {r : α → α → Prop} [i : Trichotomous r] {a b : α} :

r a b ∨ a = b ∨ r b a

source

theorem Std.trichotomous_of_rel_or_eq_or_rel_swap {α : Sort u_1} {r : α → α → Prop} (h : ∀ {a b : α}, r a b ∨ a = b ∨ r b a) :

Trichotomous r

source

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

Trichotomous r

source

theorem Std.Trichotomous.antisymm_not {α : Sort u_1} {r : α → α → Prop} [i : Trichotomous r] :

Antisymm fun (x1 x2 : α) => ¬r x1 x2

source

theorem Std.Total.rel_of_not_rel_swap {α : Sort u_1} {r : α → α → Prop} [Total r] {a b : α} (h : ¬r a b) :

r b a

source

theorem Std.total_of_not_rel_swap_imp_rel {α : Sort u_1} {r : α → α → Prop} (h : ∀ {a b : α}, ¬r a b → r b a) :

Total r

source

theorem Std.total_of_refl_of_trichotomous {α : Sort u_1} (r : α → α → Prop) [Refl r] [Trichotomous r] :

Total r

source

theorem Std.asymm_of_irrefl_of_antisymm {α : Sort u_1} (r : α → α → Prop) [Irrefl r] [Antisymm r] :

Asymm r

source

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

Asymm r

source

theorem Std.Asymm.total_not {α : Sort u_1} {r : α → α → Prop} [i : Asymm r] :

Total fun (x1 x2 : α) => ¬r x1 x2

source

instance Std.instAntisymmLeOfIsPartialOrder {α : Type u} [LE α] [IsPartialOrder α] :

Antisymm fun (x1 x2 : α) => x1 ≤ x2

source

instance Std.instTransLeOfIsPreorder {α : Type u} [LE α] [IsPreorder α] :

Trans (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

source

instance Std.instReflLeOfIsPreorder {α : Type u} [LE α] [IsPreorder α] :

Refl fun (x1 x2 : α) => x1 ≤ x2

source

instance Std.instTotalLeOfIsLinearPreorder {α : Type u} [LE α] [IsLinearPreorder α] :

Total fun (x1 x2 : α) => x1 ≤ x2

source

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

a ≤ a

source

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

a = b

source

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

source

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

source

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

a ≤ b ∨ b ≤ a

source

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

¬b ≤ a → a ≤ b

source

theorem Std.lt_trans {α : Type u} [LT α] [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

source

theorem Std.lt_iff_le_and_not_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} :

a < b ↔ a ≤ b ∧ ¬b ≤ a

source

theorem Std.not_lt_iff_not_le_or_ge {α : Type u} [LT α] [LE α] [LawfulOrderLT α] {a b : α} :

¬a < b ↔ ¬a ≤ b ∨ b ≤ a

source

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

¬b ≤ a

source

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

¬b < a

source

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

Antisymm fun (x1 x2 : α) => x1 ≤ x2

source

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

¬b < a

source

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

a ≤ b

source

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

Antisymm fun (x1 x2 : α) => x1 < x2

source

instance Std.instAsymmLtOfLawfulOrderLT {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :

Asymm fun (x1 x2 : α) => x1 < x2

source

@[deprecated Std.instIrreflOfAsymm (since := "2025-10-24")]

theorem Std.instIrreflLtOfIsPreorderOfLawfulOrderLT {α : Type u} [LT α] [LE α] [LawfulOrderLT α] :

Irrefl fun (x1 x2 : α) => x1 < x2

source

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

source

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

¬a < b ↔ b ≤ a

source

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

¬a ≤ b ↔ b < a

source

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

Trichotomous fun (x1 x2 : α) => x1 < x2

source

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

source

@[deprecated Std.Asymm.total_not (since := "2025-10-24")]

theorem Std.instTotalNotLtOfLawfulOrderLTOfLe {α : Type u} {x✝ : LT α} [LE α] [LawfulOrderLT α] :

Total fun (x1 x2 : α) => ¬x1 < x2

source

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

source

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

source

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

source

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

LT α

Equations

Instances For

source

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

Std.LawfulOrderLT α

source

theorem Std.beq_iff_le_and_ge {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] {a b : α} :

(a == b) = true ↔ a ≤ b ∧ b ≤ a

source

instance Std.instSymmEqBoolBeqTrueOfLawfulOrderBEq {α : Type u} [BEq α] [LE α] [LawfulOrderBEq α] :

Symm fun (x1 x2 : α) => (x1 == x2) = true

source

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

EquivBEq α

source

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

LawfulBEq α

source

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

BEq α

Equations

Instances For

source

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

Std.LawfulOrderBEq α

source

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

min a a = a

source

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

a ≤ min b c ↔ a ≤ b ∧ a ≤ c

source

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

min a b ≤ a

source

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

min a b ≤ b

source

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

min a b ≤ c ↔ a ≤ c ∨ b ≤ c

source

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

min a b = a ∨ min a b = b

source

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

MinEqOr α

source

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.

source

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

IdempotentOp min

source

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

Associative min

source

theorem Std.min_eq_if {α : Type u} [LE α] [DecidableLE α] {x✝ : Min α} [LawfulOrderLeftLeaningMin α] {a b : α} :

min a b = if a ≤ b then a else b

source

theorem Std.max_eq_if {α : Type u} [LE α] [DecidableLE α] {x✝ : Max α} [LawfulOrderLeftLeaningMax α] {a b : α} :

max a b = if b ≤ a then a else b

source

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

LawfulOrderLeftLeaningMin α

source

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 α

source

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

LawfulOrderLeftLeaningMin α

source

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

MinEqOr α

source

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

LawfulOrderMin α

source

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

Min α

Equations

Instances For

source

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

max a a = a

source

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

max a b ≤ c ↔ a ≤ c ∧ b ≤ c

source

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

a ≤ max a b

source

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

b ≤ max a b

source

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

a ≤ max b c ↔ a ≤ b ∨ a ≤ c

source

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

max a b = a ∨ max a b = b

source

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

MaxEqOr α

source

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.

source