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

• EmptyRelation x✝ x = False

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 , IsRefl , IsTrans : 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_1) (r : α → α → Prop) extends IsPartialOrder , IsTotal , IsPreorder , IsAntisymm , IsRefl , IsTrans : 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 , IsRefl , IsTrans : 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_1) (lt : α → α → Prop) extends IsStrictOrder , IsIrrefl , IsTrans : 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.

theorem IsStrictWeakOrder.incomp_trans {α : Sort u_1} {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 , IsIrrefl , IsTrans : 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

• ⋯ = ⋯

instance IsIrrefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsIrrefl α r] : IsIrrefl α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsRefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsRefl α r] : IsRefl α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsTrans.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] : IsTrans α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsSymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsSymm α r] : IsSymm α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsAntisymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAntisymm α r] : IsAntisymm α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsAsymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsAsymm α r] : IsAsymm α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsTotal.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTotal α r] : IsTotal α fun (a b : α) => decide (r a b) = true

Equations

• ⋯ = ⋯

instance IsTrichotomous.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrichotomous α r] : IsTrichotomous α fun (a b : α) => decide (r a b) = true

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

def Reflexive {α : Sort u_1} (r : α → α → Prop) : Prop

IsRefl as a definition, suitable for use in proofs.

Equations

• Reflexive r = ∀ (x : α), r x x

def Symmetric {α : Sort u_1} (r : α → α → Prop) : Prop

IsSymm as a definition, suitable for use in proofs.

Equations

• Symmetric r = ∀ ⦃x y : α⦄, r x y → r y x

def Transitive {α : Sort u_1} (r : α → α → Prop) : Prop

IsTrans as a definition, suitable for use in proofs.

Equations

• Transitive r = ∀ ⦃x y z : α⦄, r x y → r y z → r x z

def Irreflexive {α : Sort u_1} (r : α → α → Prop) : Prop

IsIrrefl as a definition, suitable for use in proofs.

Equations

• Irreflexive r = ∀ (x : α), ¬r x x

def AntiSymmetric {α : Sort u_1} (r : α → α → Prop) : Prop

IsAntisymm as a definition, suitable for use in proofs.

Equations

• AntiSymmetric r = ∀ ⦃x y : α⦄, r x y → r y x → x = y

def Total {α : Sort u_1} (r : α → α → Prop) : Prop

IsTotal as a definition, suitable for use in proofs.

Equations

• Total r = ∀ (x y : α), r x y ∨ r y x

@[deprecated Equivalence.refl]

theorem Equivalence.reflexive {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Reflexive r

@[deprecated Equivalence.symm]

theorem Equivalence.symmetric {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Symmetric r

@[deprecated Equivalence.trans]

theorem Equivalence.transitive {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Transitive r

@[deprecated]

theorem InvImage.trans {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) (h : Transitive r) : Transitive (InvImage r f)

@[deprecated]

theorem InvImage.irreflexive {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f)

Minimal and maximal

def Minimal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Minimal P x means that x is a minimal element satisfying P.

Equations

• Minimal P x = (P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x ≤ y)

def Maximal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Maximal P x means that x is a maximal element satisfying P.

Equations

• Maximal P x = (P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → y ≤ x)

theorem Minimal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Minimal P x) : P x

theorem Maximal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Maximal P x) : P x

theorem Minimal.le_of_le {α : Type u_1} [LE α] {P : α → Prop} {x : α} {y : α} (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y

theorem Maximal.le_of_ge {α : Type u_1} [LE α] {P : α → Prop} {x : α} {y : α} (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x

Bundled classes

Definition of Preorder and lemmas about types with a Preorder

class Preorder (α : Type u_2) extends LE , LT : 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a

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

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

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

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

The relation ≤ on a preorder is reflexive.

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

A version of le_refl where the argument is implicit

theorem le_trans {α : Type u_1} [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_1} [Preorder α] {a : α} {b : α} : a < b ↔ a ≤ b ∧ ¬b ≤ a

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

@[deprecated]

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

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

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

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

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

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

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

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

Alias of not_le_of_lt.

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

Alias of not_lt_of_le.

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

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

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

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

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

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

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

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

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

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

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

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

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

Alias of lt_asymm.

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

Alias of lt_asymm.

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

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

@[instance 900]

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

Equations

• instTransLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLtLe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransLeLt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGt_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGtGe_mathlib = { trans := ⋯ }

@[instance 900]

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

Equations

• instTransGeGt_mathlib = { trans := ⋯ }

def decidableLTOfDecidableLE {α : Type u_1} [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_2) extends Preorder , LE , LT : Type u_2

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

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

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

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

Alias of le_antisymm.

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

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

def decidableEqOfDecidableLE {α : Type u_1} [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_1} [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_1} [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_1} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : a ≤ b ↔ a < b ∨ a = b

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

theorem le_iff_lt_or_eq {α : Type u_1} [PartialOrder α] {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

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

def minDefault {α : Type u_1} [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_2) extends PartialOrder , Min , Max , Ord , Preorder , LE , LT : 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 ≤ 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_2} [self : LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b ≤ a

A linear order is total.

theorem LinearOrder.min_def {α : Type u_2} [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_2} [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_2} [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_1} [LinearOrder α] (a : α) (b : α) : a ≤ b ∨ b ≤ a

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[instance 900]

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

Equations

• instDecidableLt_mathlib a b = LinearOrder.decidableLT a b

@[instance 900]

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

Equations

• instDecidableLe_mathlib a b = LinearOrder.decidableLE a b

@[instance 900]

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

Equations

• instDecidableEq_mathlib a b = LinearOrder.decidableEq a b

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

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

Equations

• ⋯ = ⋯

def ltByCases {α : Type u_1} [LinearOrder α] (x : α) (y : α) {P : Sort u_2} (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_2} (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_2} (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_2} {β : Type u_3} [Preorder α] [LinearOrder β] {a : α} {b : α} {c : β} {d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d

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

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

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

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

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

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

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

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

theorem eq_min {α : Type u_1} [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_1} [LinearOrder α] (a : α) (b : α) : min a b = min b a

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

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

@[simp]

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

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

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

theorem eq_max {α : Type u_1} [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_1} [LinearOrder α] (a : α) (b : α) : max a b = max b a

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem cmp_eq_compare {α : Type u_1} [LinearOrder α] (a : α) (b : α) : cmp a b = compare a b

theorem cmp_eq_compareOfLessAndEq {α : Type u_1} [LinearOrder α] (a : α) (b : α) : cmp a b = compareOfLessAndEq a b

instance instLawfulCmpCompare_mathlib {α : Type u_1} [LinearOrder α] : Batteries.LawfulCmp compare

Equations

• ⋯ = ⋯

Upper and lower sets

def IsUpperSet {α : Type u_2} [LE α] (s : Set α) : Prop

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

Equations

• IsUpperSet s = ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s

def IsLowerSet {α : Type u_2} [LE α] (s : Set α) : Prop

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

Equations

• IsLowerSet s = ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s

structure UpperSet (α : Type u_2) [LE α] : Type u_2

The type of upper sets of an order.

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

• carrier : Set α

  The carrier of an UpperSet.

• upper' : IsUpperSet self.carrier

  The carrier of an UpperSet is an upper set.

theorem UpperSet.upper' {α : Type u_2} [LE α] (self : UpperSet α) : IsUpperSet self.carrier

The carrier of an UpperSet is an upper set.

structure LowerSet (α : Type u_2) [LE α] : Type u_2

The type of lower sets of an order.

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

• carrier : Set α

  The carrier of a LowerSet.

• lower' : IsLowerSet self.carrier

  The carrier of a LowerSet is a lower set.

theorem LowerSet.lower' {α : Type u_2} [LE α] (self : LowerSet α) : IsLowerSet self.carrier

The carrier of a LowerSet is a lower set.