Orders

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

Unbundled classes

class IsIrrefl (α : Sort u_1) (r : α → α → Prop) : 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

theorem IsIrrefl.irrefl {α : Sort u_1} {r : α → α → Prop} [self : IsIrrefl α r] (a : α) : ¬r a a

class IsRefl (α : Sort u_1) (r : α → α → Prop) : Prop

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

• refl : ∀ (a : α), r a a

theorem IsRefl.refl {α : Sort u_1} {r : α → α → Prop} [self : IsRefl α r] (a : α) : r a a

class IsSymm (α : Sort u_1) (r : α → α → Prop) : Prop

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

• symm : ∀ (a b : α), r a b → r b a

theorem IsSymm.symm {α : Sort u_1} {r : α → α → Prop} [self : IsSymm α r] (a : α) (b : α) : r a b → r b a

class IsAsymm (α : Sort u_1) (r : α → α → Prop) : 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

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) : Prop

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

• antisymm : ∀ (a b : α), r a b → r b a → a = b

theorem IsAntisymm.antisymm {α : Sort u_1} {r : α → α → Prop} [self : IsAntisymm α r] (a : α) (b : α) : r a b → r b a → a = b

@[instance 100]

instance IsAsymm.toIsAntisymm {α : Sort u_1} (r : α → α → Prop) [IsAsymm α r] : IsAntisymm α r

Equations

• ⋯ = ⋯

class IsTrans (α : Sort u_1) (r : α → α → Prop) : Prop

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

• trans : ∀ (a b c : α), r a b → r b c → r a c

theorem IsTrans.trans {α : Sort u_1} {r : α → α → Prop} [self : IsTrans α r] (a : α) (b : α) (c : α) : r a b → r b c → r 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) : 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

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 IsRefl , IsTrans : Prop

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

class IsPartialOrder (α : Sort u_1) (r : α → α → Prop) extends IsPreorder , IsAntisymm : Prop

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

class IsLinearOrder (α : Sort u) (r : α → α → Prop) extends IsPartialOrder , IsTotal : Prop

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

class IsEquiv (α : Sort u_1) (r : α → α → Prop) extends IsPreorder , IsSymm : Prop

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

class IsStrictOrder (α : Sort u_1) (r : α → α → Prop) extends IsIrrefl , IsTrans : Prop

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

class IsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) extends IsStrictOrder : Prop

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 b → lt b c → lt 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

theorem IsStrictWeakOrder.incomp_trans {α : Sort u} {lt : α → α → Prop} [self : IsStrictWeakOrder α lt] (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) : 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

theorem IsTrichotomous.trichotomous {α : Sort u_1} {lt : α → α → Prop} [self : IsTrichotomous α lt] (a : α) (b : α) : lt a b ∨ a = b ∨ lt b a

class IsStrictTotalOrder (α : Sort u_1) (lt : α → α → Prop) extends IsTrichotomous , IsStrictOrder : Prop

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.

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 b → r b c → r a c

theorem symm {α : Sort u_1} {r : α → α → Prop} {a : α} {b : α} [IsSymm α r] : r a b → r b a

theorem antisymm {α : Sort u_1} {r : α → α → Prop} {a : α} {b : α} [IsAntisymm α r] : r a b → r b a → a = 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} [IsTrichotomous α r] (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 b → r b c → r a c

@[elab_without_expected_type]

theorem symm_of {α : Sort u_1} (r : α → α → Prop) {a : α} {b : α} [IsSymm α r] : r a b → r 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) [IsTrichotomous α r] (a : α) (b : α) : r a b ∨ a = b ∨ r b a

Bundled classes

Definition of Preorder and lemmas about types with a Preorder

class Preorder (α : Type u) extends LE , LT : Type u

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem Preorder.le_refl {α : Type u} [self : Preorder α] (a : α) : a ≤ a

theorem Preorder.le_trans {α : Type u} [self : Preorder α] (a : α) (b : α) (c : α) : a ≤ b → b ≤ c → a ≤ c

theorem Preorder.lt_iff_le_not_le {α : Type u} [self : Preorder α] (a : α) (b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem le_refl {α : Type u} [Preorder α] (a : α) : a ≤ a

The relation ≤ on a preorder is reflexive.

theorem le_rfl {α : Type u} [Preorder α] {a : α} : a ≤ a

A version of le_refl where the argument is implicit

theorem le_trans {α : Type u} [Preorder α] {a : α} {b : α} {c : α} : a ≤ b → b ≤ c → a ≤ c

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u} [Preorder α] {a : α} {b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem lt_of_le_not_le {α : Type u} [Preorder α] {a : α} {b : α} (hab : a ≤ b) (hba : ¬b ≤ a) : a < b

@[deprecated]

theorem le_not_le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} : a < b → a ≤ b ∧ ¬b ≤ a

theorem le_of_eq {α : Type u} [Preorder α] {a : α} {b : α} (hab : a = b) : a ≤ b

theorem le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} (hab : a < b) : a ≤ b

theorem not_le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} (hab : a < b) : ¬b ≤ a

theorem not_le_of_gt {α : Type u} [Preorder α] {a : α} {b : α} (hab : a > b) : ¬a ≤ b

theorem not_lt_of_le {α : Type u} [Preorder α] {a : α} {b : α} (hab : a ≤ b) : ¬b < a

theorem not_lt_of_ge {α : Type u} [Preorder α] {a : α} {b : α} (hab : a ≥ b) : ¬a < b

theorem LT.lt.not_le {α : Type u} [Preorder α] {a : α} {b : α} (hab : a < b) : ¬b ≤ a

Alias of not_le_of_lt.

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

Alias of not_lt_of_le.

theorem ge_trans {α : Type u} [Preorder α] {a : α} {b : α} {c : α} : a ≥ b → b ≥ c → a ≥ c

theorem lt_irrefl {α : Type u} [Preorder α] (a : α) : ¬a < a

theorem gt_irrefl {α : Type u} [Preorder α] (a : α) : ¬a > a

theorem lt_of_lt_of_le {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b ≤ c) : a < c

theorem lt_of_le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b < c) : a < c

theorem gt_of_gt_of_ge {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (h₁ : a > b) (h₂ : b ≥ c) : a > c

theorem gt_of_ge_of_gt {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (h₁ : a ≥ b) (h₂ : b > c) : a > c

theorem lt_trans {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b < c) : a < c

theorem gt_trans {α : Type u} [Preorder α] {a : α} {b : α} {c : α} : a > b → b > c → a > c

theorem ne_of_lt {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : a ≠ b

theorem ne_of_gt {α : Type u} [Preorder α] {a : α} {b : α} (h : b < a) : a ≠ b

theorem lt_asymm {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : ¬b < a

theorem not_lt_of_gt {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) : ¬b < a

Alias of lt_asymm.

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

Alias of lt_asymm.

theorem le_of_lt_or_eq {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b ∨ a = b) : a ≤ b

theorem le_of_eq_or_lt {α : Type u} [Preorder α] {a : α} {b : α} (h : a = b ∨ a < b) : a ≤ b

@[instance 900]

instance instTransLe_mathlib {α : Type u} [Preorder α] : Trans LE.le LE.le LE.le

Equations

• instTransLe_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransLt_mathlib {α : Type u} [Preorder α] : Trans LT.lt LT.lt LT.lt

Equations

• instTransLt_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransLtLe_mathlib {α : Type u} [Preorder α] : Trans LT.lt LE.le LT.lt

Equations

• instTransLtLe_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransLeLt_mathlib {α : Type u} [Preorder α] : Trans LE.le LT.lt LT.lt

Equations

• instTransLeLt_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransGe_mathlib {α : Type u} [Preorder α] : Trans GE.ge GE.ge GE.ge

Equations

• instTransGe_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransGt_mathlib {α : Type u} [Preorder α] : Trans GT.gt GT.gt GT.gt

Equations

• instTransGt_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransGtGe_mathlib {α : Type u} [Preorder α] : Trans GT.gt GE.ge GT.gt

Equations

• instTransGtGe_mathlib = { trans := ⋯ }

@[instance 900]

instance instTransGeGt_mathlib {α : Type u} [Preorder α] : Trans GE.ge GT.gt GT.gt

Equations

• instTransGeGt_mathlib = { trans := ⋯ }

def decidableLTOfDecidableLE {α : Type u} [Preorder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : DecidableRel fun (x1 x2 : α) => x1 < x2

< is decidable if ≤ is.

Equations

• decidableLTOfDecidableLE x✝ x = if hab : x✝ ≤ x then if hba : x ≤ x✝ then isFalse ⋯ else isTrue ⋯ else isFalse ⋯

Definition of PartialOrder and lemmas about types with a partial order

class PartialOrder (α : Type u) extends Preorder : Type u

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

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

theorem PartialOrder.le_antisymm {α : Type u} [self : PartialOrder α] (a : α) (b : α) : a ≤ b → b ≤ a → a = b

theorem le_antisymm {α : Type u} [PartialOrder α] {a : α} {b : α} : a ≤ b → b ≤ a → a = b

theorem eq_of_le_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} : a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem le_antisymm_iff {α : Type u} [PartialOrder α] {a : α} {b : α} : a = b ↔ a ≤ b ∧ b ≤ a

theorem lt_of_le_of_ne {α : Type u} [PartialOrder α] {a : α} {b : α} : a ≤ b → a ≠ b → a < b

def decidableEqOfDecidableLE {α : Type u} [PartialOrder α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : DecidableEq α

Equality is decidable if ≤ is.

Equations

• decidableEqOfDecidableLE x✝ x = if hab : x✝ ≤ x then if hba : x ≤ x✝ then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

theorem Decidable.lt_or_eq_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) : a < b ∨ a = b

theorem Decidable.eq_or_lt_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) : a = b ∨ a < b

theorem Decidable.le_iff_lt_or_eq {α : Type u} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : a ≤ b ↔ a < b ∨ a = b

theorem lt_or_eq_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} : a ≤ b → a < b ∨ a = b

theorem le_iff_lt_or_eq {α : Type u} [PartialOrder α] {a : α} {b : α} : a ≤ b ↔ a < b ∨ a = b

Definition of LinearOrder and lemmas about types with a linear order

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

Default definition of max.

Equations

• maxDefault a b = if a ≤ b then b else a

def minDefault {α : Type u} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) : α

Default definition of min.

Equations

• minDefault a b = if a ≤ b then a else b

def tacticCompareOfLessAndEq_rfl : Lean.ParserDescr

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

• tacticCompareOfLessAndEq_rfl = Lean.ParserDescr.node `tacticCompareOfLessAndEq_rfl 1024 (Lean.ParserDescr.nonReservedSymbol "compareOfLessAndEq_rfl" false)

class LinearOrder (α : Type u) extends PartialOrder , Min , Max , Ord : Type u

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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 : 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 = compareOfLessAndEq a b

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

theorem LinearOrder.le_total {α : Type u} [self : LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b ≤ a

A linear order is total.

theorem LinearOrder.min_def {α : Type u} [self : LinearOrder α] (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} [self : LinearOrder α] (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} [self : LinearOrder α] (a : α) (b : α) : compare a b = compareOfLessAndEq a b

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

theorem le_total {α : Type u} [LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b ≤ a

theorem le_of_not_ge {α : Type u} [LinearOrder α] {a : α} {b : α} : ¬a ≥ b → a ≤ b

theorem le_of_not_le {α : Type u} [LinearOrder α] {a : α} {b : α} : ¬a ≤ b → b ≤ a

theorem lt_of_not_ge {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ¬a ≥ b) : a < b

theorem lt_trichotomy {α : Type u} [LinearOrder α] (a : α) (b : α) : a < b ∨ a = b ∨ b < a

theorem le_of_not_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ¬b < a) : a ≤ b

theorem le_of_not_gt {α : Type u} [LinearOrder α] {a : α} {b : α} : ¬a > b → a ≤ b

theorem lt_or_le {α : Type u} [LinearOrder α] (a : α) (b : α) : a < b ∨ b ≤ a

theorem le_or_lt {α : Type u} [LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b < a

theorem lt_or_ge {α : Type u} [LinearOrder α] (a : α) (b : α) : a < b ∨ a ≥ b

theorem le_or_gt {α : Type u} [LinearOrder α] (a : α) (b : α) : a ≤ b ∨ a > b

theorem lt_or_gt_of_ne {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≠ b) : a < b ∨ a > b

theorem ne_iff_lt_or_gt {α : Type u} [LinearOrder α] {a : α} {b : α} : a ≠ b ↔ a < b ∨ a > b

theorem lt_iff_not_ge {α : Type u} [LinearOrder α] (x : α) (y : α) : x < y ↔ ¬x ≥ y

@[simp]

theorem not_lt {α : Type u} [LinearOrder α] {a : α} {b : α} : ¬a < b ↔ b ≤ a

@[simp]

theorem not_le {α : Type u} [LinearOrder α] {a : α} {b : α} : ¬a ≤ b ↔ b < a

@[instance 900]

instance instDecidableLt_mathlib {α : Type u} [LinearOrder α] (a : α) (b : α) : Decidable (a < b)

Equations

• instDecidableLt_mathlib a b = LinearOrder.decidableLT a b

@[instance 900]

instance instDecidableLe_mathlib {α : Type u} [LinearOrder α] (a : α) (b : α) : Decidable (a ≤ b)

Equations

• instDecidableLe_mathlib a b = LinearOrder.decidableLE a b

@[instance 900]

instance instDecidableEq_mathlib {α : Type u} [LinearOrder α] (a : α) (b : α) : Decidable (a = b)

Equations

• instDecidableEq_mathlib a b = LinearOrder.decidableEq a b

theorem eq_or_lt_of_not_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ¬a < b) : a = b ∨ b < a

instance isStrictTotalOrder_of_linearOrder {α : Type u} [LinearOrder α] : IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2

Equations

• ⋯ = ⋯

def ltByCases {α : Type u} [LinearOrder α] (x : α) (y : α) {P : Sort u_1} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : 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₂ ⋯

Deprecated properties of inequality on Nat

@[deprecated]

def Nat.ltGeByCases {a : Nat} {b : Nat} {C : Sort u} (h₁ : a < b → C) (h₂ : b ≤ a → C) : C

Equations

• Nat.ltGeByCases h₁ h₂ = Decidable.byCases h₁ fun (h : ¬a < b) => h₂ ⋯

@[deprecated ltByCases]

def Nat.ltByCases {a : Nat} {b : Nat} {C : Sort u} (h₁ : a < b → C) (h₂ : a = b → C) (h₃ : b < a → C) : C

Equations

• Nat.ltByCases h₁ h₂ h₃ = Nat.ltGeByCases h₁ fun (h₁ : b ≤ a) => Nat.ltGeByCases h₃ fun (h : a ≤ b) => h₂ ⋯

theorem le_imp_le_of_lt_imp_lt {α : Type u_1} {β : Type u_2} [Preorder α] [LinearOrder β] {a : α} {b : α} {c : β} {d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d

theorem min_def {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b = if a ≤ b then a else b

theorem max_def {α : Type u} [LinearOrder α] (a : α) (b : α) : max a b = if a ≤ b then b else a

theorem min_le_left {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b ≤ a

theorem min_le_right {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b ≤ b

theorem le_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b

theorem le_max_left {α : Type u} [LinearOrder α] (a : α) (b : α) : a ≤ max a b

theorem le_max_right {α : Type u} [LinearOrder α] (a : α) (b : α) : b ≤ max a b

theorem max_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c

theorem eq_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) : c = min a b

theorem min_comm {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b = min b a

theorem min_assoc {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : min (min a b) c = min a (min b c)

theorem min_left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : min a (min b c) = min b (min a c)

@[simp]

theorem min_self {α : Type u} [LinearOrder α] (a : α) : min a a = a

theorem min_eq_left {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) : min a b = a

theorem min_eq_right {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b ≤ a) : min a b = b

theorem eq_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) : c = max a b

theorem max_comm {α : Type u} [LinearOrder α] (a : α) (b : α) : max a b = max b a

theorem max_assoc {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : max (max a b) c = max a (max b c)

theorem max_left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : max a (max b c) = max b (max a c)

@[simp]

theorem max_self {α : Type u} [LinearOrder α] (a : α) : max a a = a

theorem max_eq_left {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b ≤ a) : max a b = a

theorem max_eq_right {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) : max a b = b

theorem min_eq_left_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a < b) : min a b = a

theorem min_eq_right_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b < a) : min a b = b

theorem max_eq_left_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b < a) : max a b = a

theorem max_eq_right_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a < b) : max a b = b

theorem lt_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a < b) (h₂ : a < c) : a < min b c

theorem max_lt {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a < c) (h₂ : b < c) : max a b < c

theorem compare_lt_iff_lt {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.lt ↔ a < b

theorem compare_gt_iff_gt {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.gt ↔ a > b

theorem compare_eq_iff_eq {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b = Ordering.eq ↔ a = b

theorem compare_le_iff_le {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b ≠ Ordering.gt ↔ a ≤ b

theorem compare_ge_iff_ge {α : Type u} [LinearOrder α] {a : α} {b : α} : compare a b ≠ Ordering.lt ↔ a ≥ b

theorem compare_iff {α : Type u} [LinearOrder α] {o : Ordering} (a : α) (b : α) : compare a b = o ↔ o.toRel a b

instance instTransCmpCompare_mathlib {α : Type u} [LinearOrder α] : Batteries.TransCmp compare

Equations

• ⋯ = ⋯