# Orders #

Defines classes for preorders, partial orders, and linear orders and proves some basic lemmas about them.

### Unbundled classes #

def EmptyRelation {α : Sort u_1} :
ααProp

An empty relation does not relate any elements.

Equations
Instances For
class IsIrrefl (α : Sort u_1) (r : ααProp) :

IsIrrefl X r means the binary relation r on X is irreflexive (that is, r x x never holds).

• irrefl : ∀ (a : α), ¬r a a
Instances
theorem IsIrrefl.irrefl {α : Sort u_1} {r : ααProp} [self : IsIrrefl α r] (a : α) :
¬r a a
class IsRefl (α : Sort u_1) (r : ααProp) :

IsRefl X r means the binary relation r on X is reflexive.

• refl : ∀ (a : α), r a a
Instances
theorem IsRefl.refl {α : Sort u_1} {r : ααProp} [self : IsRefl α r] (a : α) :
r a a
class IsSymm (α : Sort u_1) (r : ααProp) :

IsSymm X r means the binary relation r on X is symmetric.

• symm : ∀ (a b : α), r a br b a
Instances
theorem IsSymm.symm {α : Sort u_1} {r : ααProp} [self : IsSymm α r] (a : α) (b : α) :
r a br b a
class IsAsymm (α : Sort u_1) (r : ααProp) :

IsAsymm X r means that the binary relation r on X is asymmetric, that is, r a b → ¬ r b a.

• asymm : ∀ (a b : α), r a b¬r b a
Instances
theorem IsAsymm.asymm {α : Sort u_1} {r : ααProp} [self : IsAsymm α r] (a : α) (b : α) :
r a b¬r b a
class IsAntisymm (α : Sort u_1) (r : ααProp) :

IsAntisymm X r means the binary relation r on X is antisymmetric.

• antisymm : ∀ (a b : α), r a br b aa = b
Instances
theorem IsAntisymm.antisymm {α : Sort u_1} {r : ααProp} [self : ] (a : α) (b : α) :
r a br b aa = b
@[instance 100]
instance IsAsymm.toIsAntisymm {α : Sort u_1} (r : ααProp) [IsAsymm α r] :
Equations
• =
class IsTrans (α : Sort u_1) (r : ααProp) :

IsTrans X r means the binary relation r on X is transitive.

• trans : ∀ (a b c : α), r a br b cr a c
Instances
theorem IsTrans.trans {α : Sort u_1} {r : ααProp} [self : IsTrans α r] (a : α) (b : α) (c : α) :
r a br b cr a c
instance instTransOfIsTrans {α : Sort u_1} {r : ααProp} [IsTrans α r] :
Trans r r r
Equations
• instTransOfIsTrans = { trans := }
@[instance 100]
instance instIsTransOfTrans {α : Sort u_1} {r : ααProp} [Trans r r r] :
IsTrans α r
Equations
• =
class IsTotal (α : Sort u_1) (r : ααProp) :

IsTotal X r means that the binary relation r on X is total, that is, that for any x y : X we have r x y or r y x.

• total : ∀ (a b : α), r a b r b a
Instances
theorem IsTotal.total {α : Sort u_1} {r : ααProp} [self : IsTotal α r] (a : α) (b : α) :
r a b r b a
class IsPreorder (α : Sort u_1) (r : ααProp) extends , :

IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

Instances
class IsPartialOrder (α : Sort u_1) (r : ααProp) extends , :

IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and IsAntisymm X r.

Instances
class IsLinearOrder (α : Sort u_1) (r : ααProp) extends , :

IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and IsTotal X r.

Instances
class IsEquiv (α : Sort u_1) (r : ααProp) extends , :

IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and IsSymm X r.

Instances
class IsStrictOrder (α : Sort u_1) (r : ααProp) extends , :

IsStrictOrder X r means that the binary relation r on X is a strict order, that is, IsIrrefl X r and IsTrans X r.

Instances
class IsStrictWeakOrder (α : Sort u_1) (lt : ααProp) extends :

IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a.

• irrefl : ∀ (a : α), ¬lt a a
• trans : ∀ (a b c : α), lt a blt b clt a c
• incomp_trans : ∀ (a b c : α), ¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a
Instances
theorem IsStrictWeakOrder.incomp_trans {α : Sort u_1} {lt : ααProp} [self : ] (a : α) (b : α) (c : α) :
¬lt a b ¬lt b a¬lt b c ¬lt c b¬lt a c ¬lt c a
class IsTrichotomous (α : Sort u_1) (lt : ααProp) :

IsTrichotomous X lt means that the binary relation lt on X is trichotomous, that is, either lt a b or a = b or lt b a for any a and b.

• trichotomous : ∀ (a b : α), lt a b a = b lt b a
Instances
theorem IsTrichotomous.trichotomous {α : Sort u_1} {lt : ααProp} [self : ] (a : α) (b : α) :
lt a b a = b lt b a
class IsStrictTotalOrder (α : Sort u_1) (lt : ααProp) extends , :

IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, IsTrichotomous X lt and IsStrictOrder X lt.

Instances
instance eq_isEquiv (α : Sort u_1) :
IsEquiv α fun (x1 x2 : α) => x1 = x2

Equality is an equivalence relation.

Equations
• =
theorem irrefl {α : Sort u_1} {r : ααProp} [IsIrrefl α r] (a : α) :
¬r a a
theorem refl {α : Sort u_1} {r : ααProp} [IsRefl α r] (a : α) :
r a a
theorem trans {α : Sort u_1} {r : ααProp} {a : α} {b : α} {c : α} [IsTrans α r] :
r a br b cr a c
theorem symm {α : Sort u_1} {r : ααProp} {a : α} {b : α} [IsSymm α r] :
r a br b a
theorem antisymm {α : Sort u_1} {r : ααProp} {a : α} {b : α} [] :
r a br b aa = b
theorem asymm {α : Sort u_1} {r : ααProp} {a : α} {b : α} [IsAsymm α r] :
r a b¬r b a
theorem trichotomous {α : Sort u_1} {r : ααProp} [] (a : α) (b : α) :
r a b a = b r b a
@[instance 90]
instance isAsymm_of_isTrans_of_isIrrefl {α : Sort u_1} {r : ααProp} [IsTrans α r] [IsIrrefl α r] :
IsAsymm α r
Equations
• =
@[elab_without_expected_type]
theorem irrefl_of {α : Sort u_1} (r : ααProp) [IsIrrefl α r] (a : α) :
¬r a a
@[elab_without_expected_type]
theorem refl_of {α : Sort u_1} (r : ααProp) [IsRefl α r] (a : α) :
r a a
@[elab_without_expected_type]
theorem trans_of {α : Sort u_1} (r : ααProp) {a : α} {b : α} {c : α} [IsTrans α r] :
r a br b cr a c
@[elab_without_expected_type]
theorem symm_of {α : Sort u_1} (r : ααProp) {a : α} {b : α} [IsSymm α r] :
r a br b a
@[elab_without_expected_type]
theorem asymm_of {α : Sort u_1} (r : ααProp) {a : α} {b : α} [IsAsymm α r] :
r a b¬r b a
@[elab_without_expected_type]
theorem total_of {α : Sort u_1} (r : ααProp) [IsTotal α r] (a : α) (b : α) :
r a b r b a
@[elab_without_expected_type]
theorem trichotomous_of {α : Sort u_1} (r : ααProp) [] (a : α) (b : α) :
r a b a = b r b a
def Reflexive {α : Sort u_1} (r : ααProp) :

IsRefl as a definition, suitable for use in proofs.

Equations
• = ∀ (x : α), r x x
Instances For
def Symmetric {α : Sort u_1} (r : ααProp) :

IsSymm as a definition, suitable for use in proofs.

Equations
• = ∀ ⦃x y : α⦄, r x yr y x
Instances For
def Transitive {α : Sort u_1} (r : ααProp) :

IsTrans as a definition, suitable for use in proofs.

Equations
• = ∀ ⦃x y z : α⦄, r x yr y zr x z
Instances For
def Irreflexive {α : Sort u_1} (r : ααProp) :

IsIrrefl as a definition, suitable for use in proofs.

Equations
• = ∀ (x : α), ¬r x x
Instances For
def AntiSymmetric {α : Sort u_1} (r : ααProp) :

IsAntisymm as a definition, suitable for use in proofs.

Equations
• = ∀ ⦃x y : α⦄, r x yr y xx = y
Instances For
def Total {α : Sort u_1} (r : ααProp) :

IsTotal as a definition, suitable for use in proofs.

Equations
• = ∀ (x y : α), r x y r y x
Instances For
@[deprecated Equivalence.refl]
theorem Equivalence.reflexive {α : Sort u_1} (r : ααProp) (h : ) :
@[deprecated Equivalence.symm]
theorem Equivalence.symmetric {α : Sort u_1} (r : ααProp) (h : ) :
@[deprecated Equivalence.trans]
theorem Equivalence.transitive {α : Sort u_1} (r : ααProp) (h : ) :
@[deprecated]
theorem InvImage.trans {α : Sort u_1} {β : Sort u_2} (r : ββProp) (f : αβ) (h : ) :
@[deprecated]
theorem InvImage.irreflexive {α : Sort u_1} {β : Sort u_2} (r : ββProp) (f : αβ) (h : ) :

### Definition of Preorder and lemmas about types with a Preorder#

class Preorder (α : Type u_2) extends , :
Type u_2

A preorder is a reflexive, transitive relation ≤ with a < b defined in the obvious way.

• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
Instances
theorem Preorder.le_refl {α : Type u_2} [self : ] (a : α) :
a a
theorem Preorder.le_trans {α : Type u_2} [self : ] (a : α) (b : α) (c : α) :
a bb ca c
theorem Preorder.lt_iff_le_not_le {α : Type u_2} [self : ] (a : α) (b : α) :
a < b a b ¬b a
theorem le_refl {α : Type u_1} [] (a : α) :
a a

The relation ≤ on a preorder is reflexive.

theorem le_rfl {α : Type u_1} [] {a : α} :
a a

A version of le_refl where the argument is implicit

theorem le_trans {α : Type u_1} [] {a : α} {b : α} {c : α} :
a bb ca c

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u_1} [] {a : α} {b : α} :
a < b a b ¬b a
theorem lt_of_le_not_le {α : Type u_1} [] {a : α} {b : α} (hab : a b) (hba : ¬b a) :
a < b
@[deprecated]
theorem le_not_le_of_lt {α : Type u_1} [] {a : α} {b : α} :
a < ba b ¬b a
theorem le_of_eq {α : Type u_1} [] {a : α} {b : α} (hab : a = b) :
a b
theorem le_of_lt {α : Type u_1} [] {a : α} {b : α} (hab : a < b) :
a b
theorem not_le_of_lt {α : Type u_1} [] {a : α} {b : α} (hab : a < b) :
¬b a
theorem not_le_of_gt {α : Type u_1} [] {a : α} {b : α} (hab : a > b) :
¬a b
theorem not_lt_of_le {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
¬b < a
theorem not_lt_of_ge {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
¬a < b
theorem LT.lt.not_le {α : Type u_1} [] {a : α} {b : α} (hab : a < b) :
¬b a

Alias of not_le_of_lt.

theorem LE.le.not_lt {α : Type u_1} [] {a : α} {b : α} (hab : a b) :
¬b < a

Alias of not_lt_of_le.

theorem ge_trans {α : Type u_1} [] {a : α} {b : α} {c : α} :
a bb ca c
theorem lt_irrefl {α : Type u_1} [] (a : α) :
¬a < a
theorem gt_irrefl {α : Type u_1} [] (a : α) :
¬a > a
theorem lt_of_lt_of_le {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b c) :
a < c
theorem lt_of_le_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a b) (hbc : b < c) :
a < c
theorem gt_of_gt_of_ge {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a > b) (h₂ : b c) :
a > c
theorem gt_of_ge_of_gt {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a b) (h₂ : b > c) :
a > c
theorem lt_trans {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b < c) :
a < c
theorem gt_trans {α : Type u_1} [] {a : α} {b : α} {c : α} :
a > bb > ca > c
theorem ne_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
a b
theorem ne_of_gt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
a b
theorem lt_asymm {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
¬b < a
theorem not_lt_of_gt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem not_lt_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
¬b < a

Alias of lt_asymm.

theorem le_of_lt_or_eq {α : Type u_1} [] {a : α} {b : α} (h : a < b a = b) :
a b
theorem le_of_eq_or_lt {α : Type u_1} [] {a : α} {b : α} (h : a = b a < b) :
a b
@[instance 900]
instance instTransLe_mathlib {α : Type u_1} [] :
Trans LE.le LE.le LE.le
Equations
• instTransLe_mathlib = { trans := }
@[instance 900]
instance instTransLt_mathlib {α : Type u_1} [] :
Trans LT.lt LT.lt LT.lt
Equations
• instTransLt_mathlib = { trans := }
@[instance 900]
instance instTransLtLe_mathlib {α : Type u_1} [] :
Trans LT.lt LE.le LT.lt
Equations
• instTransLtLe_mathlib = { trans := }
@[instance 900]
instance instTransLeLt_mathlib {α : Type u_1} [] :
Trans LE.le LT.lt LT.lt
Equations
• instTransLeLt_mathlib = { trans := }
@[instance 900]
instance instTransGe_mathlib {α : Type u_1} [] :
Trans GE.ge GE.ge GE.ge
Equations
• instTransGe_mathlib = { trans := }
@[instance 900]
instance instTransGt_mathlib {α : Type u_1} [] :
Trans GT.gt GT.gt GT.gt
Equations
• instTransGt_mathlib = { trans := }
@[instance 900]
instance instTransGtGe_mathlib {α : Type u_1} [] :
Trans GT.gt GE.ge GT.gt
Equations
• instTransGtGe_mathlib = { trans := }
@[instance 900]
instance instTransGeGt_mathlib {α : Type u_1} [] :
Trans GE.ge GT.gt GT.gt
Equations
• instTransGeGt_mathlib = { trans := }
def decidableLTOfDecidableLE {α : Type u_1} [] [DecidableRel fun (x1 x2 : α) => x1 x2] :
DecidableRel fun (x1 x2 : α) => x1 < x2

< is decidable if ≤ is.

Equations
• = if hab : x✝ x then if hba : x x✝ then else else
Instances For

### Definition of PartialOrder and lemmas about types with a partial order #

class PartialOrder (α : Type u_2) extends :
Type u_2

A partial order is a reflexive, transitive, antisymmetric relation ≤.

• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
Instances
theorem PartialOrder.le_antisymm {α : Type u_2} [self : ] (a : α) (b : α) :
a bb aa = b
theorem le_antisymm {α : Type u_1} [] {a : α} {b : α} :
a bb aa = b
theorem eq_of_le_of_le {α : Type u_1} [] {a : α} {b : α} :
a bb aa = b

Alias of le_antisymm.

theorem le_antisymm_iff {α : Type u_1} [] {a : α} {b : α} :
a = b a b b a
theorem lt_of_le_of_ne {α : Type u_1} [] {a : α} {b : α} :
a ba ba < b
def decidableEqOfDecidableLE {α : Type u_1} [] [DecidableRel fun (x1 x2 : α) => x1 x2] :

Equality is decidable if ≤ is.

Equations
• = if hab : x✝ x then if hba : x x✝ then else else
Instances For
theorem Decidable.lt_or_eq_of_le {α : Type u_1} [] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 x2] (hab : a b) :
a < b a = b
theorem Decidable.eq_or_lt_of_le {α : Type u_1} [] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 x2] (hab : a b) :
a = b a < b
theorem Decidable.le_iff_lt_or_eq {α : Type u_1} [] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 x2] :
a b a < b a = b
theorem lt_or_eq_of_le {α : Type u_1} [] {a : α} {b : α} :
a ba < b a = b
theorem le_iff_lt_or_eq {α : Type u_1} [] {a : α} {b : α} :
a b a < b a = b

### Definition of LinearOrder and lemmas about types with a linear order #

def maxDefault {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
α

Default definition of max.

Equations
• = if a b then b else a
Instances For
def minDefault {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
α

Default definition of min.

Equations
• = if a b then a else b
Instances For

This attempts to prove that a given instance of compare is equal to compareOfLessAndEq by introducing the arguments and trying the following approaches in order:

1. seeing if rfl works
2. seeing if the compare at hand is nonetheless essentially compareOfLessAndEq, but, because of implicit arguments, requires us to unfold the defs and split the ifs in the definition of compareOfLessAndEq
3. seeing if we can split by cases on the arguments, then see if the defs work themselves out (useful when compare is defined via a match statement, as it is for Bool)
Equations
Instances For
class LinearOrder (α : Type u_2) extends , , , :
Type u_2

A linear order is reflexive, transitive, antisymmetric and total relation ≤. We assume that every linear ordered type has decidable (≤), (<), and (=).

• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun (x1 x2 : α) => x1 x2

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
theorem LinearOrder.le_total {α : Type u_2} [self : ] (a : α) (b : α) :
a b b a

A linear order is total.

theorem LinearOrder.min_def {α : Type u_2} [self : ] (a : α) (b : α) :
min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

theorem LinearOrder.max_def {α : Type u_2} [self : ] (a : α) (b : α) :
max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

theorem LinearOrder.compare_eq_compareOfLessAndEq {α : Type u_2} [self : ] (a : α) (b : α) :
compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

theorem le_total {α : Type u_1} [] (a : α) (b : α) :
a b b a
theorem le_of_not_ge {α : Type u_1} [] {a : α} {b : α} :
¬a ba b
theorem le_of_not_le {α : Type u_1} [] {a : α} {b : α} :
¬a bb a
theorem lt_of_not_ge {α : Type u_1} [] {a : α} {b : α} (h : ¬a b) :
a < b
theorem lt_trichotomy {α : Type u_1} [] (a : α) (b : α) :
a < b a = b b < a
theorem le_of_not_lt {α : Type u_1} [] {a : α} {b : α} (h : ¬b < a) :
a b
theorem le_of_not_gt {α : Type u_1} [] {a : α} {b : α} :
¬a > ba b
theorem lt_or_le {α : Type u_1} [] (a : α) (b : α) :
a < b b a
theorem le_or_lt {α : Type u_1} [] (a : α) (b : α) :
a b b < a
theorem lt_or_ge {α : Type u_1} [] (a : α) (b : α) :
a < b a b
theorem le_or_gt {α : Type u_1} [] (a : α) (b : α) :
a b a > b
theorem lt_or_gt_of_ne {α : Type u_1} [] {a : α} {b : α} (h : a b) :
a < b a > b
theorem ne_iff_lt_or_gt {α : Type u_1} [] {a : α} {b : α} :
a b a < b a > b
theorem lt_iff_not_ge {α : Type u_1} [] (x : α) (y : α) :
x < y ¬x y
@[simp]
theorem not_lt {α : Type u_1} [] {a : α} {b : α} :
¬a < b b a
@[simp]
theorem not_le {α : Type u_1} [] {a : α} {b : α} :
¬a b b < a
@[instance 900]
instance instDecidableLt_mathlib {α : Type u_1} [] (a : α) (b : α) :
Decidable (a < b)
Equations
@[instance 900]
instance instDecidableLe_mathlib {α : Type u_1} [] (a : α) (b : α) :
Equations
@[instance 900]
instance instDecidableEq_mathlib {α : Type u_1} [] (a : α) (b : α) :
Decidable (a = b)
Equations
theorem eq_or_lt_of_not_lt {α : Type u_1} [] {a : α} {b : α} (h : ¬a < b) :
a = b b < a
instance isStrictTotalOrder_of_linearOrder {α : Type u_1} [] :
IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2
Equations
• =
def ltByCases {α : Type u_1} [] (x : α) (y : α) {P : Sort u_2} (h₁ : x < yP) (h₂ : x = yP) (h₃ : y < xP) :
P

Perform a case-split on the ordering of x and y in a decidable linear order.

Equations
• ltByCases x y h₁ h₂ h₃ = if h : x < y then h₁ h else if h' : y < x then h₃ h' else h₂
Instances For

Deprecated properties of inequality on Nat

@[deprecated]
def Nat.ltGeByCases {a : Nat} {b : Nat} {C : Sort u_2} (h₁ : a < bC) (h₂ : b aC) :
C
Equations
Instances For
@[deprecated ltByCases]
def Nat.ltByCases {a : Nat} {b : Nat} {C : Sort u_2} (h₁ : a < bC) (h₂ : a = bC) (h₃ : b < aC) :
C
Equations
Instances For
theorem le_imp_le_of_lt_imp_lt {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : α} {c : β} {d : β} (H : d < cb < a) (h : a b) :
c d
theorem min_def {α : Type u_1} [] (a : α) (b : α) :
min a b = if a b then a else b
theorem max_def {α : Type u_1} [] (a : α) (b : α) :
max a b = if a b then b else a
theorem min_le_left {α : Type u_1} [] (a : α) (b : α) :
min a b a
theorem min_le_right {α : Type u_1} [] (a : α) (b : α) :
min a b b
theorem le_min {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : c a) (h₂ : c b) :
c min a b
theorem le_max_left {α : Type u_1} [] (a : α) (b : α) :
a max a b
theorem le_max_right {α : Type u_1} [] (a : α) (b : α) :
b max a b
theorem max_le {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a c) (h₂ : b c) :
max a b c
theorem eq_min {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : c a) (h₂ : c b) (h₃ : ∀ {d : α}, d ad bd c) :
c = min a b
theorem min_comm {α : Type u_1} [] (a : α) (b : α) :
min a b = min b a
theorem min_assoc {α : Type u_1} [] (a : α) (b : α) (c : α) :
min (min a b) c = min a (min b c)
theorem min_left_comm {α : Type u_1} [] (a : α) (b : α) (c : α) :
min a (min b c) = min b (min a c)
@[simp]
theorem min_self {α : Type u_1} [] (a : α) :
min a a = a
theorem min_eq_left {α : Type u_1} [] {a : α} {b : α} (h : a b) :
min a b = a
theorem min_eq_right {α : Type u_1} [] {a : α} {b : α} (h : b a) :
min a b = b
theorem eq_max {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a c) (h₂ : b c) (h₃ : ∀ {d : α}, a db dc d) :
c = max a b
theorem max_comm {α : Type u_1} [] (a : α) (b : α) :
max a b = max b a
theorem max_assoc {α : Type u_1} [] (a : α) (b : α) (c : α) :
max (max a b) c = max a (max b c)
theorem max_left_comm {α : Type u_1} [] (a : α) (b : α) (c : α) :
max a (max b c) = max b (max a c)
@[simp]
theorem max_self {α : Type u_1} [] (a : α) :
max a a = a
theorem max_eq_left {α : Type u_1} [] {a : α} {b : α} (h : b a) :
max a b = a
theorem max_eq_right {α : Type u_1} [] {a : α} {b : α} (h : a b) :
max a b = b
theorem min_eq_left_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
min a b = a
theorem min_eq_right_of_lt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
min a b = b
theorem max_eq_left_of_lt {α : Type u_1} [] {a : α} {b : α} (h : b < a) :
max a b = a
theorem max_eq_right_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a < b) :
max a b = b
theorem lt_min {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a < b) (h₂ : a < c) :
a < min b c
theorem max_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a < c) (h₂ : b < c) :
max a b < c
theorem compare_lt_iff_lt {α : Type u_1} [] {a : α} {b : α} :
a < b
theorem compare_gt_iff_gt {α : Type u_1} [] {a : α} {b : α} :
a > b
theorem compare_eq_iff_eq {α : Type u_1} [] {a : α} {b : α} :
a = b
theorem compare_le_iff_le {α : Type u_1} [] {a : α} {b : α} :
a b
theorem compare_ge_iff_ge {α : Type u_1} [] {a : α} {b : α} :
a b
theorem compare_iff {α : Type u_1} [] (a : α) (b : α) {o : Ordering} :
compare a b = o o.Compares a b
instance instTransCmpCompare_mathlib {α : Type u_1} [] :
Equations
• =