Mathlib.Order.Compare

cmpLE definition

{α} [LE α] [DecidableLE α] (x y : α) : Ordering

Full source

/-- Like `cmp`, but uses a `≤` on the type instead of `<`. Given two elements `x` and `y`, returns a
three-way comparison result `Ordering`. -/
def cmpLE {α} [LE α] [DecidableLE α] (x y : α) : Ordering :=
  if x ≤ y then if y ≤ x then Ordering.eq else Ordering.lt else Ordering.gt

Three-way comparison via $\leq$

Informal description

Given a type $\alpha$ with a decidable less-than-or-equal relation $\leq$, the function $\text{cmpLE}$ takes two elements $x$ and $y$ in $\alpha$ and returns an `Ordering` result: - $\text{Ordering.eq}$ if $x \leq y$ and $y \leq x$ (i.e., $x = y$), - $\text{Ordering.lt}$ if $x \leq y$ but not $y \leq x$ (i.e., $x < y$), - $\text{Ordering.gt}$ otherwise (i.e., $y < x$).

cmpLE_swap theorem

{α} [LE α] [IsTotal α (· ≤ ·)] [DecidableLE α] (x y : α) : (cmpLE x y).swap = cmpLE y x

Full source

theorem cmpLE_swap {α} [LE α] [IsTotal α (· ≤ ·)] [DecidableLE α] (x y : α) :
    (cmpLE x y).swap = cmpLE y x := by
  by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, *, Ordering.swap]
  cases not_or_intro xy yx (total_of _ _ _)

Swap Property of Three-way Comparison via $\leq$

Informal description

For any type $\alpha$ with a total, decidable less-than-or-equal relation $\leq$ and any elements $x, y \in \alpha$, the swapped three-way comparison of $x$ and $y$ via $\text{cmpLE}$ equals the three-way comparison of $y$ and $x$. That is, $(\text{cmpLE}\,x\,y).\text{swap} = \text{cmpLE}\,y\,x$.

cmpLE_eq_cmp theorem

{α} [Preorder α] [IsTotal α (· ≤ ·)] [DecidableLE α] [DecidableLT α] (x y : α) : cmpLE x y = cmp x y

Full source

theorem cmpLE_eq_cmp {α} [Preorder α] [IsTotal α (· ≤ ·)] [DecidableLE α] [DecidableLT α]
    (x y : α) : cmpLE x y = cmp x y := by
  by_cases xy : x ≤ y <;> by_cases yx : y ≤ x <;> simp [cmpLE, lt_iff_le_not_le, *, cmp, cmpUsing]
  cases not_or_intro xy yx (total_of _ _ _)

Equivalence of Three-way Comparisons: $\text{cmpLE} = \text{cmp}$ in Total Preorders

Informal description

For any type $\alpha$ with a preorder $\leq$ that is total and decidable, and with a decidable strict order $<$, the three-way comparison function $\text{cmpLE}$ (based on $\leq$) coincides with the standard comparison function $\text{cmp}$ (based on $<$) for any two elements $x, y \in \alpha$. That is, $\text{cmpLE}(x, y) = \text{cmp}(x, y)$.

Ordering.compares_swap theorem

[LT α] {a b : α} {o : Ordering} : o.swap.Compares a b ↔ o.Compares b a

Full source

theorem compares_swap [LT α] {a b : α} {o : Ordering} : o.swap.Compares a b ↔ o.Compares b a := by
  cases o
  · exact Iff.rfl
  · exact eq_comm
  · exact Iff.rfl

Swapped Ordering Comparison Equivalence

Informal description

For any ordering `o` and elements `a`, `b` in a type `α` with a strict order `<`, the statement that the swapped ordering `o.swap` compares `a` and `b` is equivalent to the statement that the original ordering `o` compares `b` and `a`.

Ordering.swap_eq_iff_eq_swap theorem

{o o' : Ordering} : o.swap = o' ↔ o = o'.swap

Full source

theorem swap_eq_iff_eq_swap {o o' : Ordering} : o.swap = o' ↔ o = o'.swap := by
  rw [← swap_inj, swap_swap]

Equivalence of Ordering Swaps: $o.\text{swap} = o' \leftrightarrow o = o'.\text{swap}$

Informal description

For any two orderings $o$ and $o'$, the swap of $o$ equals $o'$ if and only if $o$ equals the swap of $o'$. In other words, $o.\text{swap} = o' \leftrightarrow o = o'.\text{swap}$.

Ordering.Compares.ne_lt theorem

[Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o ≠ lt ↔ b ≤ a)

Full source

theorem Compares.ne_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o ≠ lto ≠ lt ↔ b ≤ a)
  | lt, _, _, h => ⟨absurd rfl, fun h' => (not_le_of_lt h h').elim⟩
  | eq, _, _, h => ⟨fun _ => ge_of_eq h, fun _ h => by injection h⟩
  | gt, _, _, h => ⟨fun _ => le_of_lt h, fun _ h => by injection h⟩

Comparison Result: $o \neq \text{lt}$ iff $b \leq a$ in a Preorder

Informal description

Let $\alpha$ be a preorder, and let $a, b \in \alpha$. For any ordering $o$, if $o$ compares $a$ and $b$, then $o$ is not the less-than ordering if and only if $b \leq a$.

Ordering.Compares.ne_gt theorem

[Preorder α] {o} {a b : α} (h : Compares o a b) : o ≠ gt ↔ a ≤ b

Full source

theorem Compares.ne_gt [Preorder α] {o} {a b : α} (h : Compares o a b) : o ≠ gto ≠ gt ↔ a ≤ b :=
  (not_congr swap_eq_iff_eq_swap.symm).trans h.swap.ne_lt

Comparison Result: $o \neq \text{gt}$ iff $a \leq b$ in a Preorder

Informal description

Let $\alpha$ be a preorder, and let $a, b \in \alpha$. For any ordering $o$, if $o$ compares $a$ and $b$, then $o$ is not the greater-than ordering if and only if $a \leq b$.

Ordering.Compares.le_total theorem

[Preorder α] {a b : α} : ∀ {o}, Compares o a b → a ≤ b ∨ b ≤ a

Full source

theorem Compares.le_total [Preorder α] {a b : α} : ∀ {o}, Compares o a b → a ≤ b ∨ b ≤ a
  | lt, h => Or.inl (le_of_lt h)
  | eq, h => Or.inl (le_of_eq h)
  | gt, h => Or.inr (le_of_lt h)

Total Ordering Property for Compared Elements in a Preorder

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$, if there exists an ordering $o$ such that $o$ compares $a$ and $b$, then either $a \leq b$ or $b \leq a$ holds.

Ordering.Compares.le_antisymm theorem

[Preorder α] {a b : α} : ∀ {o}, Compares o a b → a ≤ b → b ≤ a → a = b

Full source

theorem Compares.le_antisymm [Preorder α] {a b : α} : ∀ {o}, Compares o a b → a ≤ b → b ≤ a → a = b
  | lt, h, _, hba => (not_le_of_lt h hba).elim
  | eq, h, _, _ => h
  | gt, h, hab, _ => (not_le_of_lt h hab).elim

Antisymmetry of Ordering Comparison in Preorders

Informal description

Let $\alpha$ be a type with a preorder $\leq$. For any elements $a, b \in \alpha$ and any ordering comparison result $o$, if $o$ compares $a$ and $b$ (i.e., $\text{Compares}\, o\, a\, b$ holds), and both $a \leq b$ and $b \leq a$ hold, then $a = b$.

Ordering.Compares.inj theorem

[Preorder α] {o₁} : ∀ {o₂} {a b : α}, Compares o₁ a b → Compares o₂ a b → o₁ = o₂

Full source

theorem Compares.inj [Preorder α] {o₁} :
    ∀ {o₂} {a b : α}, Compares o₁ a b → Compares o₂ a b → o₁ = o₂
  | lt, _, _, h₁, h₂ => h₁.eq_lt.2 h₂
  | eq, _, _, h₁, h₂ => h₁.eq_eq.2 h₂
  | gt, _, _, h₁, h₂ => h₁.eq_gt.2 h₂

Uniqueness of Ordering Comparison in Preorders

Informal description

Let $\alpha$ be a type with a preorder. For any two elements $a, b \in \alpha$ and any two orderings $o_1, o_2$, if $o_1$ compares $a$ and $b$ (i.e., $a < b$, $a = b$, or $a > b$ according to $o_1$) and $o_2$ also compares $a$ and $b$, then $o_1 = o_2$.

Ordering.compares_iff_of_compares_impl theorem

 [LinearOrder α] [Preorder β] {a b : α} {a' b' : β} (h : ∀ {o}, Compares o a b → Compares o a' b') (o) :
  Compares o a b ↔ Compares o a' b'

Full source

theorem compares_iff_of_compares_impl [LinearOrder α] [Preorder β] {a b : α} {a' b' : β}
    (h : ∀ {o}, Compares o a b → Compares o a' b') (o) : ComparesCompares o a b ↔ Compares o a' b' := by
  refine ⟨h, fun ho => ?_⟩
  rcases lt_trichotomy a b with hab | hab | hab
  · have hab : Compares Ordering.lt a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.eq a b := hab
    rwa [ho.inj (h hab)]
  · have hab : Compares Ordering.gt a b := hab
    rwa [ho.inj (h hab)]

Equivalence of Order Comparisons under Implication in Linear and Preorders

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ a preordered type. For any elements $a, b \in \alpha$ and $a', b' \in \beta$, if for every ordering $o$, the comparison of $a$ and $b$ under $o$ implies the comparison of $a'$ and $b'$ under $o$, then for any fixed ordering $o$, the comparison of $a$ and $b$ under $o$ holds if and only if the comparison of $a'$ and $b'$ under $o$ holds. In other words, $\text{Compares}\, o\, a\, b \leftrightarrow \text{Compares}\, o\, a'\, b'$.

toDual_compares_toDual theorem

[LT α] {a b : α} {o : Ordering} : Compares o (toDual a) (toDual b) ↔ Compares o b a

Full source

@[simp]
theorem toDual_compares_toDual [LT α] {a b : α} {o : Ordering} :
    ComparesCompares o (toDual a) (toDual b) ↔ Compares o b a := by
  cases o
  exacts [Iff.rfl, eq_comm, Iff.rfl]

Comparison of Dual Elements is Equivalent to Reversed Comparison of Original Elements

Informal description

Let $\alpha$ be a type with a strict order relation $<$. For any elements $a, b \in \alpha$ and any ordering $o$, the comparison of the dual elements $\text{toDual}(a)$ and $\text{toDual}(b)$ under $o$ holds if and only if the comparison of $b$ and $a$ under $o$ holds. In other words, $\text{Compares}\, o\, (\text{toDual}(a))\, (\text{toDual}(b)) \leftrightarrow \text{Compares}\, o\, b\, a$.

ofDual_compares_ofDual theorem

[LT α] {a b : αᵒᵈ} {o : Ordering} : Compares o (ofDual a) (ofDual b) ↔ Compares o b a

Full source

@[simp]
theorem ofDual_compares_ofDual [LT α] {a b : αᵒᵈ} {o : Ordering} :
    ComparesCompares o (ofDual a) (ofDual b) ↔ Compares o b a := by
  cases o
  exacts [Iff.rfl, eq_comm, Iff.rfl]

Comparison Reversal under Dual Order Construction

Informal description

Let $\alpha$ be a type with a strict order relation $<$. For any elements $a, b$ in the dual order $\alpha^\text{op}$ and any ordering $o$, the comparison of $\text{ofDual}(a)$ and $\text{ofDual}(b)$ under $o$ holds if and only if the comparison of $b$ and $a$ under $o$ holds. In other words, $\text{Compares}\, o\, (\text{ofDual}(a))\, (\text{ofDual}(b)) \leftrightarrow \text{Compares}\, o\, b\, a$.

cmp_compares theorem

[LinearOrder α] (a b : α) : (cmp a b).Compares a b

Full source

theorem cmp_compares [LinearOrder α] (a b : α) : (cmp a b).Compares a b := by
  obtain h | h | h := lt_trichotomy a b <;> simp [cmp, cmpUsing, h, h.not_lt]

Comparison Function Correctly Relates Elements in Linear Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\mathrm{cmp}(a, b)$ correctly relates $a$ and $b$ according to the ordering relation (either $a < b$, $a = b$, or $a > b$).

Ordering.Compares.cmp_eq theorem

[LinearOrder α] {a b : α} {o : Ordering} (h : o.Compares a b) : cmp a b = o

Full source

theorem Ordering.Compares.cmp_eq [LinearOrder α] {a b : α} {o : Ordering} (h : o.Compares a b) :
    cmp a b = o :=
  (cmp_compares a b).inj h

Comparison Function Correctness: $\mathrm{cmp}(a, b) = o$ when $o$ compares $a$ and $b$

Informal description

Let $\alpha$ be a linearly ordered type. For any elements $a, b \in \alpha$ and any ordering $o$, if $o$ correctly compares $a$ and $b$ (i.e., $o$ represents the true ordering relation between $a$ and $b$), then the comparison function $\mathrm{cmp}(a, b)$ returns $o$.

cmp_swap theorem

[Preorder α] [DecidableLT α] (a b : α) : (cmp a b).swap = cmp b a

Full source

@[simp]
theorem cmp_swap [Preorder α] [DecidableLT α] (a b : α) : (cmp a b).swap = cmp b a := by
  unfold cmp cmpUsing
  by_cases h : a < b <;> by_cases h₂ : b < a <;> simp [h, h₂, Ordering.swap]
  exact lt_asymm h h₂

Comparison Swap Property: $\text{cmp}(a, b).\text{swap} = \text{cmp}(b, a)$

Informal description

For any two elements $a$ and $b$ in a preorder $\alpha$ with decidable strict order relation, the comparison result of $a$ and $b$ after swapping is equal to the comparison result of $b$ and $a$. That is, $\text{cmp}(a, b).\text{swap} = \text{cmp}(b, a)$.

cmpLE_toDual theorem

[LE α] [DecidableLE α] (x y : α) : cmpLE (toDual x) (toDual y) = cmpLE y x

Full source

@[simp]
theorem cmpLE_toDual [LE α] [DecidableLE α] (x y : α) : cmpLE (toDual x) (toDual y) = cmpLE y x :=
  rfl

Comparison via $\leq$ under Order Duality: $\text{cmpLE}(\text{toDual}\,x, \text{toDual}\,y) = \text{cmpLE}(y, x)$

Informal description

For any type $\alpha$ with a decidable less-than-or-equal relation $\leq$, and for any elements $x, y$ in $\alpha$, the comparison via $\leq$ of their images under the order duality map $\text{toDual}$ is equal to the comparison via $\leq$ of $y$ and $x$ in the original order. That is, $\text{cmpLE}(\text{toDual}\,x, \text{toDual}\,y) = \text{cmpLE}(y, x)$.

cmpLE_ofDual theorem

[LE α] [DecidableLE α] (x y : αᵒᵈ) : cmpLE (ofDual x) (ofDual y) = cmpLE y x

Full source

@[simp]
theorem cmpLE_ofDual [LE α] [DecidableLE α] (x y : αᵒᵈ) : cmpLE (ofDual x) (ofDual y) = cmpLE y x :=
  rfl

Comparison via $\leq$ under Order Duality: $\text{cmpLE}(\text{ofDual}\,x, \text{ofDual}\,y) = \text{cmpLE}(y, x)$

Informal description

For any type $\alpha$ with a decidable less-than-or-equal relation $\leq$, and for any elements $x, y$ in the order dual $\alpha^{\text{op}}$, the comparison via $\leq$ of their images under the order duality map $\text{ofDual}$ is equal to the comparison via $\leq$ of $y$ and $x$ in the original order. That is, $\text{cmpLE}(\text{ofDual}\,x, \text{ofDual}\,y) = \text{cmpLE}(y, x)$.

cmp_toDual theorem

[LT α] [DecidableLT α] (x y : α) : cmp (toDual x) (toDual y) = cmp y x

Full source

@[simp]
theorem cmp_toDual [LT α] [DecidableLT α] (x y : α) : cmp (toDual x) (toDual y) = cmp y x :=
  rfl

Comparison under Order Duality: $\text{cmp}(\text{toDual}\,x, \text{toDual}\,y) = \text{cmp}(y, x)$

Informal description

For any type $\alpha$ with a decidable strict order relation $<$, and for any elements $x, y$ in $\alpha$, the comparison of their images under the order duality map $\text{toDual}$ is equal to the comparison of $y$ and $x$ in the original order. That is, $\text{cmp}(\text{toDual}\,x, \text{toDual}\,y) = \text{cmp}(y, x)$.

cmp_ofDual theorem

[LT α] [DecidableLT α] (x y : αᵒᵈ) : cmp (ofDual x) (ofDual y) = cmp y x

Full source

@[simp]
theorem cmp_ofDual [LT α] [DecidableLT α] (x y : αᵒᵈ) : cmp (ofDual x) (ofDual y) = cmp y x :=
  rfl

Comparison under Order Duality: $\text{cmp}(\text{ofDual}\,x, \text{ofDual}\,y) = \text{cmp}(y, x)$

Informal description

For any type $\alpha$ with a decidable strict order relation $<$, and for any elements $x, y$ in the order dual $\alpha^{\text{op}}$, the comparison of their images under the order duality map $\text{ofDual}$ is equal to the comparison of $y$ and $x$ in the original order. That is, $\text{cmp}(\text{ofDual}\,x, \text{ofDual}\,y) = \text{cmp}(y, x)$.

linearOrderOfCompares definition

[Preorder α] (cmp : α → α → Ordering) (h : ∀ a b, (cmp a b).Compares a b) : LinearOrder α

Full source

/-- Generate a linear order structure from a preorder and `cmp` function. -/
def linearOrderOfCompares [Preorder α] (cmp : α → α → Ordering)
    (h : ∀ a b, (cmp a b).Compares a b) : LinearOrder α :=
  let H : DecidableLE α := fun a b => decidable_of_iff _ (h a b).ne_gt
  { inferInstanceAs (Preorder α) with
    le_antisymm := fun a b => (h a b).le_antisymm,
    le_total := fun a b => (h a b).le_total,
    toMin := minOfLe,
    toMax := maxOfLe,
    toDecidableLE := H,
    toDecidableLT := fun a b => decidable_of_iff _ (h a b).eq_lt,
    toDecidableEq := fun a b => decidable_of_iff _ (h a b).eq_eq }

Linear order from comparison function

Informal description

Given a preorder on a type $\alpha$ and a comparison function $\text{cmp} : \alpha \to \alpha \to \text{Ordering}$ such that for any two elements $a, b \in \alpha$, the result of $\text{cmp}\, a\, b$ determines whether $a < b$, $a = b$, or $a > b$, this definition constructs a linear order on $\alpha$ extending the given preorder. The linear order is defined by using the comparison function to decide the order relations and equality.

cmp_eq_lt_iff theorem

: cmp x y = Ordering.lt ↔ x < y

Full source

@[simp]
theorem cmp_eq_lt_iff : cmpcmp x y = Ordering.lt ↔ x < y :=
  Ordering.Compares.eq_lt (cmp_compares x y)

Comparison Yields Less-Than if and Only if Elements are Ordered as Such

Informal description

For any two elements $x$ and $y$ in a linearly ordered type $\alpha$, the comparison function $\mathrm{cmp}(x, y)$ returns $\mathrm{Ordering.lt}$ if and only if $x < y$.

cmp_eq_eq_iff theorem

: cmp x y = Ordering.eq ↔ x = y

Full source

@[simp]
theorem cmp_eq_eq_iff : cmpcmp x y = Ordering.eq ↔ x = y :=
  Ordering.Compares.eq_eq (cmp_compares x y)

Comparison Function Equality Criterion: $\mathrm{cmp}(x, y) = \mathrm{eq} \leftrightarrow x = y$

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, the comparison function $\mathrm{cmp}(x, y)$ returns $\mathrm{Ordering.eq}$ if and only if $x = y$.

cmp_eq_gt_iff theorem

: cmp x y = Ordering.gt ↔ y < x

Full source

@[simp]
theorem cmp_eq_gt_iff : cmpcmp x y = Ordering.gt ↔ y < x :=
  Ordering.Compares.eq_gt (cmp_compares x y)

Comparison Yields Greater-Than if and Only if Reverse Order Holds

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, the comparison function $\mathrm{cmp}(x, y)$ returns $\mathrm{Ordering.gt}$ if and only if $y < x$.

cmp_self_eq_eq theorem

: cmp x x = Ordering.eq

Full source

@[simp]
theorem cmp_self_eq_eq : cmp x x = Ordering.eq := by rw [cmp_eq_eq_iff]

Reflexive Comparison Yields Equality: $\mathrm{cmp}(x, x) = \mathrm{eq}$

Informal description

For any element $x$ in a linearly ordered type, the comparison function $\mathrm{cmp}(x, x)$ returns $\mathrm{Ordering.eq}$.

cmp_eq_cmp_symm theorem

: cmp x y = cmp x' y' ↔ cmp y x = cmp y' x'

Full source

theorem cmp_eq_cmp_symm : cmpcmp x y = cmp x' y' ↔ cmp y x = cmp y' x' :=
  ⟨fun h => by rwa [← cmp_swap x', ← cmp_swap, swap_inj],
   fun h => by rwa [← cmp_swap y', ← cmp_swap, swap_inj]⟩

Symmetric Comparison Equality: $\text{cmp}(x,y) = \text{cmp}(x',y') \leftrightarrow \text{cmp}(y,x) = \text{cmp}(y',x')$

Informal description

For any elements $x, y, x', y'$ in a preorder with decidable strict order relation, the comparison result $\text{cmp}(x, y)$ is equal to $\text{cmp}(x', y')$ if and only if the comparison result $\text{cmp}(y, x)$ is equal to $\text{cmp}(y', x')$.

lt_iff_lt_of_cmp_eq_cmp theorem

(h : cmp x y = cmp x' y') : x < y ↔ x' < y'

Full source

theorem lt_iff_lt_of_cmp_eq_cmp (h : cmp x y = cmp x' y') : x < y ↔ x' < y' := by
  rw [← cmp_eq_lt_iff, ← cmp_eq_lt_iff, h]

Strict Order Preservation Under Equal Comparisons: $x < y \leftrightarrow x' < y'$ when $\mathrm{cmp}(x,y) = \mathrm{cmp}(x',y')$

Informal description

For any elements $x, y, x', y'$ in a linear order, if the comparison results satisfy $\mathrm{cmp}(x, y) = \mathrm{cmp}(x', y')$, then $x < y$ if and only if $x' < y'$.

le_iff_le_of_cmp_eq_cmp theorem

(h : cmp x y = cmp x' y') : x ≤ y ↔ x' ≤ y'

Full source

theorem le_iff_le_of_cmp_eq_cmp (h : cmp x y = cmp x' y') : x ≤ y ↔ x' ≤ y' := by
  rw [← not_lt, ← not_lt]
  apply not_congr
  apply lt_iff_lt_of_cmp_eq_cmp
  rwa [cmp_eq_cmp_symm]

Non-Strict Order Preservation Under Equal Comparisons: $x \leq y \leftrightarrow x' \leq y'$ when $\mathrm{cmp}(x,y) = \mathrm{cmp}(x',y')$

Informal description

For any elements $x, y, x', y'$ in a linear order, if the comparison results satisfy $\mathrm{cmp}(x, y) = \mathrm{cmp}(x', y')$, then $x \leq y$ if and only if $x' \leq y'$.

LT.lt.cmp_eq_lt theorem

(h : x < y) : cmp x y = Ordering.lt

Full source

theorem LT.lt.cmp_eq_lt (h : x < y) : cmp x y = Ordering.lt :=
  (cmp_eq_lt_iff _ _).2 h

Comparison Yields Less-Than for Strictly Ordered Elements

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, if $x < y$, then the comparison function $\mathrm{cmp}(x, y)$ returns $\mathrm{Ordering.lt}$.

LT.lt.cmp_eq_gt theorem

(h : x < y) : cmp y x = Ordering.gt

Full source

theorem LT.lt.cmp_eq_gt (h : x < y) : cmp y x = Ordering.gt :=
  (cmp_eq_gt_iff _ _).2 h

Comparison Yields Greater-Than for Reversed Elements in Strict Order

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, if $x < y$, then the comparison function $\mathrm{cmp}(y, x)$ returns $\mathrm{Ordering.gt}$.

Eq.cmp_eq_eq theorem

(h : x = y) : cmp x y = Ordering.eq

Full source

theorem Eq.cmp_eq_eq (h : x = y) : cmp x y = Ordering.eq :=
  (cmp_eq_eq_iff _ _).2 h

Comparison Yields Equality for Equal Elements

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, if $x = y$, then the comparison function $\mathrm{cmp}(x, y)$ returns $\mathrm{Ordering.eq}$.

Eq.cmp_eq_eq' theorem

(h : x = y) : cmp y x = Ordering.eq

Full source

theorem Eq.cmp_eq_eq' (h : x = y) : cmp y x = Ordering.eq :=
  h.symm.cmp_eq_eq

Comparison Yields Equality for Reversed Equal Elements

Informal description

For any two elements $x$ and $y$ in a linearly ordered type, if $x = y$, then the comparison function $\mathrm{cmp}(y, x)$ returns $\mathrm{Ordering.eq}$.

Definitions