doc-next-gen

Mathlib.Order.Defs.PartialOrder

Module docstring

{"# Orders

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

We also define covering relations on a preorder. We say that b covers a if a < b and there is no element in between. We say that b weakly covers a if a ≤ b and there is no element between a and b. In a partial order this is equivalent to a ⋖ b ∨ a = b, in a preorder this is equivalent to a ⋖ b ∨ (a ≤ b ∧ b ≤ a)

Notation

  • a ⋖ b means that b covers a.
  • a ⩿ b means that b weakly covers a. ","### Definition of Preorder and lemmas about types with a Preorder ","### Definition of PartialOrder and lemmas about types with a partial order "}
Preorder structure
(α : Type*) extends LE α, LT α
Full source 
/-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
class Preorder (α : Type*) extends LE α, LT α where
  le_refl : ∀ a : α, a ≤ a
  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
  lt := fun a b => a ≤ b ∧ ¬b ≤ a
  lt_iff_le_not_le : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
Preorder
Informal description
A preorder on a type $\alpha$ is a reflexive and transitive binary relation $\leq$ with a derived strict order $<$ defined in the usual way (i.e., $a < b$ if $a \leq b$ and $a \neq b$).
le_refl theorem
: ∀ a : α, a ≤ a
Full source 
/-- The relation `≤` on a preorder is reflexive. -/
@[refl, simp] lemma le_refl : ∀ a : α, a ≤ a := Preorder.le_refl
Reflexivity of the $\leq$ relation in a preorder
Informal description
For any element $a$ in a preorder, the relation $\leq$ is reflexive, i.e., $a \leq a$.
le_rfl theorem
: a ≤ a
Full source 
/-- A version of `le_refl` where the argument is implicit -/
lemma le_rfl : a ≤ a := le_refl a
Reflexivity of the $\leq$ relation in a preorder (implicit argument version)
Informal description
For any element $a$ in a preorder, the relation $\leq$ is reflexive, i.e., $a \leq a$.
le_trans theorem
: a ≤ b → b ≤ c → a ≤ c
Full source 
/-- The relation `≤` on a preorder is transitive. -/
lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
Transitivity of the $\leq$ relation in a preorder
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a \leq b$ and $b \leq c$, then $a \leq c$.
lt_iff_le_not_le theorem
: a < b ↔ a ≤ b ∧ ¬b ≤ a
Full source 
lemma lt_iff_le_not_le : a < b ↔ a ≤ b ∧ ¬b ≤ a := Preorder.lt_iff_le_not_le _ _
Characterization of Strict Order in Terms of Non-Strict Order
Informal description
For any elements $a$ and $b$ in a preorder, $a < b$ if and only if $a \leq b$ and it is not the case that $b \leq a$.
lt_of_le_not_le theorem
(hab : a ≤ b) (hba : ¬b ≤ a) : a < b
Full source 
lemma lt_of_le_not_le (hab : a ≤ b) (hba : ¬ b ≤ a) : a < b := lt_iff_le_not_le.2 ⟨hab, hba⟩
Strict Order from Non-Strict Order and Non-Reflexivity
Informal description
For any elements $a$ and $b$ in a preorder, if $a \leq b$ and it is not the case that $b \leq a$, then $a < b$.
le_of_eq theorem
(hab : a = b) : a ≤ b
Full source 
lemma le_of_eq (hab : a = b) : a ≤ b := by rw [hab]
Equality Implies Non-Strict Order: $a = b \implies a \leq b$
Informal description
For any elements $a$ and $b$ in a preorder, if $a = b$, then $a \leq b$.
le_of_lt theorem
(hab : a < b) : a ≤ b
Full source 
lemma le_of_lt (hab : a < b) : a ≤ b := (lt_iff_le_not_le.1 hab).1
Strict Order Implies Non-Strict Order: $a < b \implies a \leq b$
Informal description
For any elements $a$ and $b$ in a preorder, if $a < b$, then $a \leq b$.
not_le_of_lt theorem
(hab : a < b) : ¬b ≤ a
Full source 
lemma not_le_of_lt (hab : a < b) : ¬ b ≤ a := (lt_iff_le_not_le.1 hab).2
Strict Order Implies Non-Reflexive Order: $a < b \implies \neg (b \leq a)$
Informal description
For any elements $a$ and $b$ in a preorder, if $a < b$, then it is not the case that $b \leq a$.
not_le_of_gt theorem
(hab : a > b) : ¬a ≤ b
Full source 
lemma not_le_of_gt (hab : a > b) : ¬a ≤ b := not_le_of_lt hab
Strict Greater-Than Implies Non-Reflexive Order: $a > b \implies \neg (a \leq b)$
Informal description
For any elements $a$ and $b$ in a preorder, if $a > b$, then it is not the case that $a \leq b$.
not_lt_of_le theorem
(hab : a ≤ b) : ¬b < a
Full source 
lemma not_lt_of_le (hab : a ≤ b) : ¬ b < a := imp_not_comm.1 not_le_of_lt hab
Non-strict Order Implies Non-strict Reverse Order: $a \leq b \implies \neg (b < a)$
Informal description
For any elements $a$ and $b$ in a preorder, if $a \leq b$, then it is not the case that $b < a$.
not_lt_of_ge theorem
(hab : a ≥ b) : ¬a < b
Full source 
lemma not_lt_of_ge (hab : a ≥ b) : ¬a < b := not_lt_of_le hab
Non-strict Greater-Than Implies Non-strict Order: $a \geq b \implies \neg (a < b)$
Informal description
For any elements $a$ and $b$ in a preorder, if $a \geq b$, then it is not the case that $a < b$.
ge_trans theorem
: a ≥ b → b ≥ c → a ≥ c
Full source 
lemma ge_trans : a ≥ b → b ≥ c → a ≥ c := fun h₁ h₂ => le_trans h₂ h₁
Transitivity of the $\geq$ relation in a preorder
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a \geq b$ and $b \geq c$, then $a \geq c$.
lt_irrefl theorem
(a : α) : ¬a < a
Full source 
lemma lt_irrefl (a : α) : ¬a < a := fun h ↦ not_le_of_lt h le_rfl
Irreflexivity of the Strict Order Relation: $\neg (a < a)$
Informal description
For any element $a$ in a preorder, it is not the case that $a < a$.
gt_irrefl theorem
(a : α) : ¬a > a
Full source 
lemma gt_irrefl (a : α) : ¬a > a := lt_irrefl _
Irreflexivity of the Strict Greater-Than Relation: $\neg (a > a)$
Informal description
For any element $a$ in a preorder, it is not the case that $a > a$.
lt_of_lt_of_le theorem
(hab : a < b) (hbc : b ≤ c) : a < c
Full source 
lemma lt_of_lt_of_le (hab : a < b) (hbc : b ≤ c) : a < c :=
  lt_of_le_not_le (le_trans (le_of_lt hab) hbc) fun hca ↦ not_le_of_lt hab (le_trans hbc hca)
Transitivity of Strict and Non-Strict Order: $a < b \land b \leq c \implies a < c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a < b$ and $b \leq c$, then $a < c$.
lt_of_le_of_lt theorem
(hab : a ≤ b) (hbc : b < c) : a < c
Full source 
lemma lt_of_le_of_lt (hab : a ≤ b) (hbc : b < c) : a < c :=
  lt_of_le_not_le (le_trans hab (le_of_lt hbc)) fun hca ↦ not_le_of_lt hbc (le_trans hca hab)
Transitivity of Mixed Inequalities: $a \leq b < c \implies a < c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a \leq b$ and $b < c$, then $a < c$.
gt_of_gt_of_ge theorem
(h₁ : a > b) (h₂ : b ≥ c) : a > c
Full source 
lemma gt_of_gt_of_ge (h₁ : a > b) (h₂ : b ≥ c) : a > c := lt_of_le_of_lt h₂ h₁
Transitivity of Mixed Inequalities: $a > b \geq c \implies a > c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a > b$ and $b \geq c$, then $a > c$.
gt_of_ge_of_gt theorem
(h₁ : a ≥ b) (h₂ : b > c) : a > c
Full source 
lemma gt_of_ge_of_gt (h₁ : a ≥ b) (h₂ : b > c) : a > c := lt_of_lt_of_le h₂ h₁
Transitivity of Mixed Inequalities: $a \geq b > c \implies a > c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a \geq b$ and $b > c$, then $a > c$.
lt_trans theorem
(hab : a < b) (hbc : b < c) : a < c
Full source 
lemma lt_trans (hab : a < b) (hbc : b < c) : a < c := lt_of_lt_of_le hab (le_of_lt hbc)
Transitivity of Strict Order: $a < b < c \implies a < c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a < b$ and $b < c$, then $a < c$.
gt_trans theorem
: a > b → b > c → a > c
Full source 
lemma gt_trans : a > b → b > c → a > c := fun h₁ h₂ => lt_trans h₂ h₁
Transitivity of Greater-Than Relation: $a > b > c \implies a > c$
Informal description
For any elements $a$, $b$, and $c$ in a preorder, if $a > b$ and $b > c$, then $a > c$.
ne_of_lt theorem
(h : a < b) : a ≠ b
Full source 
lemma ne_of_lt (h : a < b) : a ≠ b := fun he => absurd h (he ▸ lt_irrefl a)
Inequality from Strict Order: $a < b \Rightarrow a \neq b$
Informal description
For any elements $a$ and $b$ in a preorder, if $a < b$ then $a \neq b$.
ne_of_gt theorem
(h : b < a) : a ≠ b
Full source 
lemma ne_of_gt (h : b < a) : a ≠ b := fun he => absurd h (he ▸ lt_irrefl a)
Inequality from Greater-Than Relation: $b < a \implies a \neq b$
Informal description
For any elements $a$ and $b$ in a preorder, if $b < a$, then $a \neq b$.
lt_asymm theorem
(h : a < b) : ¬b < a
Full source 
lemma lt_asymm (h : a < b) : ¬b < a := fun h1 : b < a => lt_irrefl a (lt_trans h h1)
Asymmetry of Strict Order: $a < b \implies \neg(b < a)$
Informal description
For any elements $a$ and $b$ in a preorder, if $a < b$ then it is not the case that $b < a$.
le_of_lt_or_eq theorem
(h : a < b ∨ a = b) : a ≤ b
Full source 
lemma le_of_lt_or_eq (h : a < b ∨ a = b) : a ≤ b := h.elim le_of_lt le_of_eq
Non-Strict Order from Strict Order or Equality: $a < b \lor a = b \implies a \leq b$
Informal description
For any elements $a$ and $b$ in a preorder, if $a < b$ or $a = b$, then $a \leq b$.
le_of_eq_or_lt theorem
(h : a = b ∨ a < b) : a ≤ b
Full source 
lemma le_of_eq_or_lt (h : a = b ∨ a < b) : a ≤ b := h.elim le_of_eq le_of_lt
Non-strict Order from Equality or Strict Order: $a = b ∨ a < b → a ≤ b$
Informal description
For any elements $a$ and $b$ in a preorder, if $a = b$ or $a < b$, then $a \leq b$.
instTransLe_mathlib instance
: @Trans α α α LE.le LE.le LE.le
Full source 
instance (priority := 900) : @Trans α α α LE.le LE.le LE.le := ⟨le_trans⟩
Transitivity of the $\leq$ Relation in a Preorder
Informal description
For any type $\alpha$ with a preorder, the relation $\leq$ is transitive. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a \leq b$ and $b \leq c$, then $a \leq c$.
instTransLt_mathlib instance
: @Trans α α α LT.lt LT.lt LT.lt
Full source 
instance (priority := 900) : @Trans α α α LT.lt LT.lt LT.lt := ⟨lt_trans⟩
Transitivity of the Strict Order Relation
Informal description
For any type $\alpha$ with a preorder, the strict order relation $<$ is transitive. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a < b$ and $b < c$, then $a < c$.
instTransLtLe_mathlib instance
: @Trans α α α LT.lt LE.le LT.lt
Full source 
instance (priority := 900) : @Trans α α α LT.lt LE.le LT.lt := ⟨lt_of_lt_of_le⟩
Transitivity of $<$ with respect to $\leq$ in a preorder
Informal description
For any type $\alpha$ with a preorder, the relation $<$ is transitive with respect to $\leq$. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a < b$ and $b \leq c$, then $a < c$.
instTransLeLt_mathlib instance
: @Trans α α α LE.le LT.lt LT.lt
Full source 
instance (priority := 900) : @Trans α α α LE.le LT.lt LT.lt := ⟨lt_of_le_of_lt⟩
Transitivity of $\leq$ and $<$ in a Preorder
Informal description
For any type $\alpha$ with a preorder, the relation $\leq$ followed by $<$ implies $<$. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a \leq b$ and $b < c$, then $a < c$.
instTransGe_mathlib instance
: @Trans α α α GE.ge GE.ge GE.ge
Full source 
instance (priority := 900) : @Trans α α α GE.ge GE.ge GE.ge := ⟨ge_trans⟩
Transitivity of the $\geq$ Relation in a Preorder
Informal description
For any type $\alpha$ with a preorder, the relation $\geq$ is transitive. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a \geq b$ and $b \geq c$, then $a \geq c$.
instTransGt_mathlib instance
: @Trans α α α GT.gt GT.gt GT.gt
Full source 
instance (priority := 900) : @Trans α α α GT.gt GT.gt GT.gt := ⟨gt_trans⟩
Transitivity of the Greater-Than Relation in Preorders
Informal description
For any type $\alpha$ with a preorder, the relation $>$ is transitive. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a > b$ and $b > c$, then $a > c$.
instTransGtGe_mathlib instance
: @Trans α α α GT.gt GE.ge GT.gt
Full source 
instance (priority := 900) : @Trans α α α GT.gt GE.ge GT.gt := ⟨gt_of_gt_of_ge⟩
Transitivity of $>$ with respect to $\geq$ in a preorder
Informal description
For any type $\alpha$ with a preorder, the relation $>$ is transitive with respect to $\geq$. That is, for any elements $a$, $b$, and $c$ in $\alpha$, if $a > b$ and $b \geq c$, then $a > c$.
instTransGeGt_mathlib instance
: @Trans α α α GE.ge GT.gt GT.gt
Full source 
instance (priority := 900) : @Trans α α α GE.ge GT.gt GT.gt := ⟨gt_of_ge_of_gt⟩
Transitivity of $\geq$ and $>$ in Preorders
Informal description
For any type $\alpha$ with a preorder, the relation $\geq$ is transitive with respect to $>$, meaning that if $a \geq b$ and $b > c$, then $a > c$.
decidableLTOfDecidableLE definition
[DecidableLE α] : DecidableLT α
Full source 
/-- `<` is decidable if `≤` is. -/
def decidableLTOfDecidableLE [DecidableLE α] : DecidableLT α
  | a, b =>
    if hab : a ≤ b then
      if hba : b ≤ a then isFalse fun hab' => not_le_of_gt hab' hba
      else isTrue <| lt_of_le_not_le hab hba
    else isFalse fun hab' => hab (le_of_lt hab')
Decidability of strict order from non-strict order
Informal description
Given a type $\alpha$ with a decidable preorder relation $\leq$, the strict order relation $<$ is also decidable. Specifically, for any elements $a$ and $b$ in $\alpha$, the decidability of $a < b$ is derived from the decidability of $a \leq b$ and $b \leq a$ as follows: - If $a \leq b$ and $\neg (b \leq a)$, then $a < b$ is true. - If $a \leq b$ and $b \leq a$, then $a < b$ is false. - If $\neg (a \leq b)$, then $a < b$ is false.
WCovBy definition
(a b : α) : Prop
Full source 
/-- `WCovBy a b` means that `a = b` or `b` covers `a`.
This means that `a ≤ b` and there is no element in between.
-/
def WCovBy (a b : α) : Prop :=
  a ≤ b ∧ ∀ ⦃c⦄, a < c → ¬c < b
Weak covering relation in a preorder
Informal description
For elements $a$ and $b$ in a preorder $\alpha$, we say $b$ *weakly covers* $a$ (denoted $a \ ⩿ \ b$) if $a \leq b$ and there exists no element $c$ strictly between them (i.e., there is no $c$ such that $a < c < b$).
term_⩿_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for `WCovBy a b`. -/
infixl:50 " ⩿ " => WCovBy
Weakly covers notation
Informal description
The notation `a ⩿ b` denotes that `b` weakly covers `a`, meaning `a ≤ b` and there is no element strictly between `a` and `b` in the preorder.
CovBy definition
{α : Type*} [LT α] (a b : α) : Prop
Full source 
/-- `CovBy a b` means that `b` covers `a`: `a < b` and there is no element in between. -/
def CovBy {α : Type*} [LT α] (a b : α) : Prop :=
  a < b ∧ ∀ ⦃c⦄, a < c → ¬c < b
Covering relation \( a \lessdot b \)
Informal description
For elements \( a \) and \( b \) in a type \( \alpha \) with a strict order relation \( < \), we say that \( b \) covers \( a \) (denoted \( a \lessdot b \)) if \( a < b \) and there is no element \( c \) such that \( a < c < b \).
term_⋖_ definition
: Lean.TrailingParserDescr✝
Full source 
/-- Notation for `CovBy a b`. -/
infixl:50 " ⋖ " => CovBy
Covering relation notation (`a ⋖ b`)
Informal description
The notation `a ⋖ b` represents the covering relation `CovBy a b`, meaning that `b` covers `a` in the given order.
PartialOrder structure
(α : Type*) extends Preorder α
Full source 
/-- A partial order is a reflexive, transitive, antisymmetric relation `≤`. -/
class PartialOrder (α : Type*) extends Preorder α where
  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
Partial Order
Informal description
A partial order on a type $\alpha$ is a reflexive, transitive, and antisymmetric binary relation $\leq$. This extends the structure of a preorder by adding the antisymmetry condition: if $a \leq b$ and $b \leq a$, then $a = b$.
le_antisymm theorem
: a ≤ b → b ≤ a → a = b
Full source 
lemma le_antisymm : a ≤ b → b ≤ a → a = b := PartialOrder.le_antisymm _ _
Antisymmetry of Partial Order: $a \leq b \land b \leq a \implies a = b$
Informal description
For any elements $a$ and $b$ in a partially ordered set, if $a \leq b$ and $b \leq a$, then $a = b$.
lt_of_le_of_ne theorem
: a ≤ b → a ≠ b → a < b
Full source 
lemma lt_of_le_of_ne : a ≤ b → a ≠ b → a < b := fun h₁ h₂ =>
  lt_of_le_not_le h₁ <| mt (le_antisymm h₁) h₂
Strict Order from Non-Strict Order and Inequality: $a \leq b \land a \neq b \implies a < b$
Informal description
For any elements $a$ and $b$ in a partially ordered set, if $a \leq b$ and $a \neq b$, then $a < b$.
decidableEqOfDecidableLE definition
[DecidableLE α] : DecidableEq α
Full source 
/-- Equality is decidable if `≤` is. -/
def decidableEqOfDecidableLE [DecidableLE α] : DecidableEq α
  | a, b =>
    if hab : a ≤ b then
      if hba : b ≤ a then isTrue (le_antisymm hab hba) else isFalse fun heq => hba (heq ▸ le_refl _)
    else isFalse fun heq => hab (heq ▸ le_refl _)
Decidability of equality from decidability of partial order
Informal description
Given a type $\alpha$ with a decidable partial order $\leq$, the equality of any two elements $a$ and $b$ in $\alpha$ is decidable. Specifically, if $a \leq b$ and $b \leq a$ are both true, then $a = b$; otherwise, $a \neq b$.
Decidable.le_iff_lt_or_eq theorem
: a ≤ b ↔ a < b ∨ a = b
Full source 
lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b :=
  ⟨lt_or_eq_of_le, le_of_lt_or_eq⟩
Decidable Order Characterization: $a \leq b \leftrightarrow (a < b \lor a = b)$
Informal description
For any elements $a$ and $b$ in a partially ordered set with decidable order, the non-strict inequality $a \leq b$ holds if and only if either $a < b$ or $a = b$.
lt_or_eq_of_le theorem
: a ≤ b → a < b ∨ a = b
Full source 
lemma lt_or_eq_of_le : a ≤ b → a < b ∨ a = b := open scoped Classical in Decidable.lt_or_eq_of_le
Order Trichotomy: $a \leq b \implies a < b \lor a = b$
Informal description
For any elements $a$ and $b$ in a partially ordered set, if $a \leq b$, then either $a < b$ or $a = b$.
le_iff_lt_or_eq theorem
: a ≤ b ↔ a < b ∨ a = b
Full source 
lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := open scoped Classical in Decidable.le_iff_lt_or_eq
Order Characterization: $a \leq b \leftrightarrow (a < b \lor a = b)$
Informal description
For any elements $a$ and $b$ in a partially ordered set, the non-strict inequality $a \leq b$ holds if and only if either $a < b$ or $a = b$.