Mathlib.Order.Defs.LinearOrder

maxDefault definition

[LE α] [DecidableLE α] (a b : α)

Full source

/-- Default definition of `max`. -/
def maxDefault [LE α] [DecidableLE α] (a b : α) :=
  if a ≤ b then b else a

Maximum function (default implementation)

Informal description

Given a type $\alpha$ with a linear order and decidable less-than-or-equal relation, the function $\max(a, b)$ returns the greater of two elements $a$ and $b$ according to the order on $\alpha$. The default implementation checks whether $a \leq b$ and returns $b$ if true, otherwise returns $a$.

minDefault definition

[LE α] [DecidableLE α] (a b : α)

Full source

/-- Default definition of `min`. -/
def minDefault [LE α] [DecidableLE α] (a b : α) :=
  if a ≤ b then a else b

Default minimum function

Informal description

The default definition of the minimum function for a type $\alpha$ with a linear order and decidable less-than-or-equal relation. For any two elements $a, b \in \alpha$, it returns $a$ if $a \leq b$ and $b$ otherwise.

tacticCompareOfLessAndEq_rfl definition

: Lean.ParserDescr✝

Full source

macromacro "compareOfLessAndEq_rfl" : tactic =>
  `(tactic| (intros a b; first | rfl |
    (simp only [compare, compareOfLessAndEq]; split_ifs <;> rfl) |
    (induction a <;> induction b <;> simp +decide only)))

Tactic for proving equality of `compare` and `compareOfLessAndEq`

Informal description

The tactic `compareOfLessAndEq_rfl` attempts to prove that a given instance of the `compare` function is equal to `compareOfLessAndEq` by introducing the arguments and applying the following strategies in order: 1. Attempting to use reflexivity (`rfl`). 2. Unfolding the definitions of `compare` and `compareOfLessAndEq` and splitting on the `if` conditions if necessary. 3. Splitting by cases on the arguments and simplifying the definitions (useful when `compare` is defined via pattern matching, as in `Bool`).

LinearOrder structure

(α : Type*) extends PartialOrder α, Min α, Max α, Ord α

Full source

/-- A linear order is reflexive, transitive, antisymmetric and total relation `≤`.
We assume that every linear ordered type has decidable `(≤)`, `(<)`, and `(=)`. -/
class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α where
  /-- A linear order is total. -/
  le_total (a b : α) : a ≤ b ∨ b ≤ a
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableLE : DecidableLE α
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableEq : DecidableEq α := @decidableEqOfDecidableLE _ _ toDecidableLE
  /-- In a linearly ordered type, we assume the order relations are all decidable. -/
  toDecidableLT : DecidableLT α := @decidableLTOfDecidableLE _ _ toDecidableLE
  min := fun a b => if a ≤ b then a else b
  max := fun a b => if a ≤ b then b else a
  /-- The minimum function is equivalent to the one you get from `minOfLe`. -/
  min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
  /-- The minimum function is equivalent to the one you get from `maxOfLe`. -/
  max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
  compare a b := compareOfLessAndEq a b
  /-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`. -/
  compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by
    compareOfLessAndEq_rfl

Linear Order Structure

Informal description

A linear order on a type $\alpha$ is a reflexive, transitive, antisymmetric, and total relation $\leq$. It extends a partial order and includes operations for minimum (`Min`), maximum (`Max`), and ordering (`Ord`). Additionally, every linear order is assumed to have decidable $\leq$, $<$, and $=$ relations.

le_total theorem

: ∀ a b : α, a ≤ b ∨ b ≤ a

Full source

lemma le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := LinearOrder.le_total

Total Order Property: $a \leq b$ or $b \leq a$ for any $a, b$ in a linear order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a \leq b$ or $b \leq a$ holds.

le_of_not_ge theorem

: ¬a ≥ b → a ≤ b

Full source

lemma le_of_not_ge : ¬a ≥ b → a ≤ b := (le_total b a).resolve_left

Implication from Non-Greater-Than to Less-Than-Or-Equal in Linear Orders

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, if $a$ is not greater than or equal to $b$ (i.e., $\neg (a \geq b)$), then $a \leq b$.

le_of_not_le theorem

: ¬a ≤ b → b ≤ a

Full source

lemma le_of_not_le : ¬a ≤ b → b ≤ a := (le_total a b).resolve_left

Implication from Non-Less-Than-Or-Equal to Greater-Than-Or-Equal in Linear Orders

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, if $a$ is not less than or equal to $b$ (i.e., $\neg (a \leq b)$), then $b \leq a$.

lt_of_not_ge theorem

(h : ¬a ≥ b) : a < b

Full source

lemma lt_of_not_ge (h : ¬a ≥ b) : a < b := lt_of_le_not_le (le_of_not_ge h) h

Strict inequality from non-greater-than in linear orders: $\neg (a \geq b) \Rightarrow a < b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, if $a$ is not greater than or equal to $b$ (i.e., $\neg (a \geq b)$), then $a < b$.

lt_trichotomy theorem

(a b : α) : a < b ∨ a = b ∨ b < a

Full source

lemma lt_trichotomy (a b : α) : a < b ∨ a = b ∨ b < a :=
  Or.elim (le_total a b)
    (fun h : a ≤ b =>
      Or.elim (Decidable.lt_or_eq_of_le h) (fun h : a < b => Or.inl h) fun h : a = b =>
        Or.inr (Or.inl h))
    fun h : b ≤ a =>
    Or.elim (Decidable.lt_or_eq_of_le h) (fun h : b < a => Or.inr (Or.inr h)) fun h : b = a =>
      Or.inr (Or.inl h.symm)

Trichotomy Property for Linear Orders: $a < b \lor a = b \lor b < a$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, exactly one of the following holds: $a < b$, $a = b$, or $b < a$.

le_of_not_lt theorem

(h : ¬b < a) : a ≤ b

Full source

lemma le_of_not_lt (h : ¬b < a) : a ≤ b :=
  match lt_trichotomy a b with
  | Or.inl hlt => le_of_lt hlt
  | Or.inr (Or.inl HEq) => HEq ▸ le_refl a
  | Or.inr (Or.inr hgt) => absurd hgt h

Non-strict inequality from negation of strict inequality: $\neg (b < a) \Rightarrow a \leq b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, if it is not the case that $b < a$, then $a \leq b$.

le_of_not_gt theorem

: ¬a > b → a ≤ b

Full source

lemma le_of_not_gt : ¬a > b → a ≤ b := le_of_not_lt

Non-strict inequality from negation of strict reverse inequality: $\neg (a > b) \Rightarrow a \leq b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, if it is not the case that $a > b$, then $a \leq b$.

lt_or_le theorem

(a b : α) : a < b ∨ b ≤ a

Full source

lemma lt_or_le (a b : α) : a < b ∨ b ≤ a :=
  if hba : b ≤ a then Or.inr hba else Or.inl <| lt_of_not_ge hba

Trichotomy: $a < b$ or $b \leq a$ in linear orders

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a < b$ or $b \leq a$ holds.

le_or_lt theorem

(a b : α) : a ≤ b ∨ b < a

Full source

lemma le_or_lt (a b : α) : a ≤ b ∨ b < a := (lt_or_le b a).symm

Linear Order Trichotomy: $a \leq b$ or $b < a$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a \leq b$ or $b < a$ holds.

lt_or_ge theorem

: ∀ a b : α, a < b ∨ a ≥ b

Full source

lemma lt_or_ge : ∀ a b : α, a < b ∨ a ≥ b := lt_or_le

Trichotomy: $a < b$ or $a \geq b$ in linear orders

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a < b$ or $a \geq b$ holds.

le_or_gt theorem

: ∀ a b : α, a ≤ b ∨ a > b

Full source

lemma le_or_gt : ∀ a b : α, a ≤ b ∨ a > b := le_or_lt

Linear Order Dichotomy: $a \leq b$ or $a > b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a \leq b$ or $a > b$ holds.

lt_or_gt_of_ne theorem

(h : a ≠ b) : a < b ∨ a > b

Full source

lemma lt_or_gt_of_ne (h : a ≠ b) : a < b ∨ a > b := by simpa [h] using lt_trichotomy a b

Trichotomy for Distinct Elements in Linear Orders: $a \neq b \to (a < b) \lor (a > b)$

Informal description

For any two distinct elements $a$ and $b$ in a linearly ordered type $\alpha$, either $a < b$ or $a > b$.

ne_iff_lt_or_gt theorem

: a ≠ b ↔ a < b ∨ a > b

Full source

lemma ne_iff_lt_or_gt : a ≠ ba ≠ b ↔ a < b ∨ a > b := ⟨lt_or_gt_of_ne, (Or.elim · ne_of_lt ne_of_gt)⟩

Inequality Characterization in Linear Orders: $a \neq b \leftrightarrow (a < b) \lor (a > b)$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the inequality $a \neq b$ holds if and only if either $a < b$ or $a > b$.

lt_iff_not_ge theorem

(x y : α) : x < y ↔ ¬x ≥ y

Full source

lemma lt_iff_not_ge (x y : α) : x < y ↔ ¬x ≥ y := ⟨not_le_of_gt, lt_of_not_ge⟩

Characterization of Strict Inequality via Non-Greater-Than: $x < y \leftrightarrow \neg (x \geq y)$

Informal description

For any two elements $x$ and $y$ in a linearly ordered type $\alpha$, the strict inequality $x < y$ holds if and only if $x$ is not greater than or equal to $y$ (i.e., $\neg (x \geq y)$).

not_lt theorem

: ¬a < b ↔ b ≤ a

Full source

@[simp] lemma not_lt : ¬a < b¬a < b ↔ b ≤ a := ⟨le_of_not_gt, not_lt_of_ge⟩

Negation of Strict Inequality: $\neg (a < b) \leftrightarrow b \leq a$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the negation of the strict inequality $a < b$ is equivalent to the non-strict inequality $b \leq a$, i.e., $\neg (a < b) \leftrightarrow b \leq a$.

not_le theorem

: ¬a ≤ b ↔ b < a

Full source

@[simp] lemma not_le : ¬a ≤ b¬a ≤ b ↔ b < a := (lt_iff_not_ge _ _).symm

Negation of Order Relation: $\neg (a \leq b) \leftrightarrow b < a$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the negation of $a \leq b$ is equivalent to $b < a$, i.e., $\neg (a \leq b) \leftrightarrow b < a$.

ltByCases definition

(x y : α) {P : Sort*} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : P

Full source

/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order. -/
def ltByCases (x y : α) {P : Sort*} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) : P :=
  if h : x < y then h₁ h
  else if h' : y < x then h₃ h' else h₂ (le_antisymm (le_of_not_gt h') (le_of_not_gt h))

Case split on ordering of two elements in a linear order

Informal description

Given two elements $x$ and $y$ in a decidable linear order $\alpha$, and three functions $h_1$, $h_2$, and $h_3$ producing a result of type $P$ for the cases $x < y$, $x = y$, and $y < x$ respectively, this function performs a case split based on the ordering of $x$ and $y$ and returns the corresponding result.

le_imp_le_of_lt_imp_lt theorem

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

Full source

theorem le_imp_le_of_lt_imp_lt {α β} [Preorder α] [LinearOrder β] {a b : α} {c d : β}
    (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
  le_of_not_lt fun h' => not_le_of_gt (H h') h

Order Reversal Implication: $d < c \implies b < a$ and $a \leq b$ implies $c \leq d$

Informal description

Let $\alpha$ be a preorder and $\beta$ a linear order. For any elements $a, b \in \alpha$ and $c, d \in \beta$, if the implication $d < c \implies b < a$ holds and $a \leq b$, then $c \leq d$.

min_def theorem

(a b : α) : min a b = if a ≤ b then a else b

Full source

lemma min_def (a b : α) : min a b = if a ≤ b then a else b := by rw [LinearOrder.min_def a]

Definition of Minimum in a Linear Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the minimum of $a$ and $b$ is defined as $a$ if $a \leq b$, and $b$ otherwise. In other words, $\min(a, b) = \begin{cases} a & \text{if } a \leq b \\ b & \text{otherwise} \end{cases}$.

max_def theorem

(a b : α) : max a b = if a ≤ b then b else a

Full source

lemma max_def (a b : α) : max a b = if a ≤ b then b else a := by rw [LinearOrder.max_def a]

Definition of Maximum in a Linear Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the maximum of $a$ and $b$ is defined as $b$ if $a \leq b$, and $a$ otherwise. In other words, $\max(a, b) = \begin{cases} b & \text{if } a \leq b \\ a & \text{otherwise} \end{cases}$.

min_le_left theorem

(a b : α) : min a b ≤ a

Full source

lemma min_le_left (a b : α) : min a b ≤ a := by
  if h : a ≤ b
  then simp [min_def, if_pos h, le_refl]
  else simpa [min_def, if_neg h] using le_of_not_le h

Minimum is Less Than or Equal to First Argument

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the minimum of $a$ and $b$ is less than or equal to $a$, i.e., $\min(a, b) \leq a$.

min_le_right theorem

(a b : α) : min a b ≤ b

Full source

lemma min_le_right (a b : α) : min a b ≤ b := by
  if h : a ≤ b
  then simpa [min_def, if_pos h] using h
  else simp [min_def, if_neg h, le_refl]

Minimum is Less Than or Equal to Right Argument

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the minimum of $a$ and $b$ is less than or equal to $b$, i.e., $\min(a, b) \leq b$.

le_min theorem

(h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b

Full source

lemma le_min (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b := by
  if h : a ≤ b
  then simpa [min_def, if_pos h] using h₁
  else simpa [min_def, if_neg h] using h₂

Minimum is the Greatest Lower Bound in a Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, if $c \leq a$ and $c \leq b$, then $c \leq \min(a, b)$.

le_max_left theorem

(a b : α) : a ≤ max a b

Full source

lemma le_max_left (a b : α) : a ≤ max a b := by
  if h : a ≤ b
  then simpa [max_def, if_pos h] using h
  else simp [max_def, if_neg h, le_refl]

Left Element is Less Than or Equal to Maximum

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the element $a$ is less than or equal to the maximum of $a$ and $b$, i.e., $a \leq \max(a, b)$.

le_max_right theorem

(a b : α) : b ≤ max a b

Full source

lemma le_max_right (a b : α) : b ≤ max a b := by
  if h : a ≤ b
  then simp [max_def, if_pos h, le_refl]
  else simpa [max_def, if_neg h] using le_of_not_le h

Right Element is Less Than or Equal to Maximum in Linear Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the element $b$ is less than or equal to the maximum of $a$ and $b$, i.e., $b \leq \max(a, b)$.

max_le theorem

(h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c

Full source

lemma max_le (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c := by
  if h : a ≤ b
  then simpa [max_def, if_pos h] using h₂
  else simpa [max_def, if_neg h] using h₁

Maximum is Least Upper Bound in Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, if $a \leq c$ and $b \leq c$, then $\max(a, b) \leq c$.

min_comm theorem

(a b : α) : min a b = min b a

Full source

lemma min_comm (a b : α) : min a b = min b a :=
  eq_min (min_le_right a b) (min_le_left a b) fun h₁ h₂ => le_min h₂ h₁

Commutativity of Minimum in Linear Order

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the minimum of $a$ and $b$ is equal to the minimum of $b$ and $a$, i.e., $\min(a, b) = \min(b, a)$.

min_assoc theorem

(a b c : α) : min (min a b) c = min a (min b c)

Full source

lemma min_assoc (a b c : α) : min (min a b) c = min a (min b c) := by
  apply eq_min
  · apply le_trans (min_le_left ..) (min_le_left ..)
  · apply le_min
    · apply le_trans (min_le_left ..) (min_le_right ..)
    · apply min_le_right
  · intro d h₁ h₂; apply le_min
    · apply le_min h₁; apply le_trans h₂; apply min_le_left
    · apply le_trans h₂; apply min_le_right

Associativity of Minimum Operation in a Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, the minimum operation is associative, i.e., $\min(\min(a, b), c) = \min(a, \min(b, c))$.

min_left_comm theorem

(a b c : α) : min a (min b c) = min b (min a c)

Full source

lemma min_left_comm (a b c : α) : min a (min b c) = min b (min a c) := by
  rw [← min_assoc, min_comm a, min_assoc]

Left-Commutativity of Minimum Operation in Linear Order

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, the minimum operation satisfies the left-commutativity property: $\min(a, \min(b, c)) = \min(b, \min(a, c))$.

min_self theorem

(a : α) : min a a = a

Full source

@[simp] lemma min_self (a : α) : min a a = a := by simp [min_def]

Idempotence of Minimum: $\min(a, a) = a$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the minimum of $a$ and itself is equal to $a$, i.e., $\min(a, a) = a$.

min_eq_left theorem

(h : a ≤ b) : min a b = a

Full source

lemma min_eq_left (h : a ≤ b) : min a b = a := by
  apply Eq.symm; apply eq_min (le_refl _) h; intros; assumption

Minimum of Two Elements Equals the Smaller One

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, if $a \leq b$, then the minimum of $a$ and $b$ is equal to $a$.

min_eq_right theorem

(h : b ≤ a) : min a b = b

Full source

lemma min_eq_right (h : b ≤ a) : min a b = b := min_comm b a ▸ min_eq_left h

Minimum of Two Elements Equals the Smaller One (Symmetric Case)

Informal description

For any elements $a$ and $b$ in a linearly ordered type $\alpha$, if $b \leq a$, then the minimum of $a$ and $b$ is equal to $b$.

max_comm theorem

(a b : α) : max a b = max b a

Full source

lemma max_comm (a b : α) : max a b = max b a :=
  eq_max (le_max_right a b) (le_max_left a b) fun h₁ h₂ => max_le h₂ h₁

Commutativity of Maximum: $\max(a, b) = \max(b, a)$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the maximum of $a$ and $b$ is equal to the maximum of $b$ and $a$, i.e., $\max(a, b) = \max(b, a)$.

max_assoc theorem

(a b c : α) : max (max a b) c = max a (max b c)

Full source

lemma max_assoc (a b c : α) : max (max a b) c = max a (max b c) := by
  apply eq_max
  · apply le_trans (le_max_left a b) (le_max_left ..)
  · apply max_le
    · apply le_trans (le_max_right a b) (le_max_left ..)
    · apply le_max_right
  · intro d h₁ h₂; apply max_le
    · apply max_le h₁; apply le_trans (le_max_left _ _) h₂
    · apply le_trans (le_max_right _ _) h₂

Associativity of Maximum: $\max(\max(a, b), c) = \max(a, \max(b, c))$

Informal description

For any three elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, the maximum operation is associative, i.e., $\max(\max(a, b), c) = \max(a, \max(b, c))$.

max_left_comm theorem

(a b c : α) : max a (max b c) = max b (max a c)

Full source

lemma max_left_comm (a b c : α) : max a (max b c) = max b (max a c) := by
  rw [← max_assoc, max_comm a, max_assoc]

Left-Commutativity of Maximum: $\max(a, \max(b, c)) = \max(b, \max(a, c))$

Informal description

For any three elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, the maximum operation satisfies the left-commutativity property: $\max(a, \max(b, c)) = \max(b, \max(a, c))$.

max_self theorem

(a : α) : max a a = a

Full source

@[simp] lemma max_self (a : α) : max a a = a := by simp [max_def]

Idempotence of Maximum: $\max(a, a) = a$

Informal description

For any element $a$ in a linearly ordered type $\alpha$, the maximum of $a$ with itself is equal to $a$, i.e., $\max(a, a) = a$.

max_eq_left theorem

(h : b ≤ a) : max a b = a

Full source

lemma max_eq_left (h : b ≤ a) : max a b = a := by
  apply Eq.symm; apply eq_max (le_refl _) h; intros; assumption

Maximum of Two Elements When One is Less Than or Equal to the Other

Informal description

For any elements $a$ and $b$ in a linearly ordered set, if $b \leq a$, then the maximum of $a$ and $b$ is equal to $a$, i.e., $\max(a, b) = a$.

max_eq_right theorem

(h : a ≤ b) : max a b = b

Full source

lemma max_eq_right (h : a ≤ b) : max a b = b := max_comm b a ▸ max_eq_left h

Maximum of Two Elements When One is Less Than or Equal to the Other (Symmetric Case)

Informal description

For any elements $a$ and $b$ in a linearly ordered set, if $a \leq b$, then the maximum of $a$ and $b$ is equal to $b$, i.e., $\max(a, b) = b$.

min_eq_left_of_lt theorem

(h : a < b) : min a b = a

Full source

lemma min_eq_left_of_lt (h : a < b) : min a b = a := min_eq_left (le_of_lt h)

Minimum of Two Elements Under Strict Inequality: $\min(a, b) = a$ when $a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered type, if $a < b$, then the minimum of $a$ and $b$ is equal to $a$, i.e., $\min(a, b) = a$.

min_eq_right_of_lt theorem

(h : b < a) : min a b = b

Full source

lemma min_eq_right_of_lt (h : b < a) : min a b = b := min_eq_right (le_of_lt h)

Minimum Identity for Strictly Ordered Elements: $\min(a, b) = b$ when $b < a$

Informal description

For any elements $a$ and $b$ in a linearly ordered type, if $b < a$, then the minimum of $a$ and $b$ is equal to $b$, i.e., $\min(a, b) = b$.

max_eq_left_of_lt theorem

(h : b < a) : max a b = a

Full source

lemma max_eq_left_of_lt (h : b < a) : max a b = a := max_eq_left (le_of_lt h)

Maximum Identity for Strictly Ordered Elements: $\max(a, b) = a$ when $b < a$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, if $b < a$, then the maximum of $a$ and $b$ is equal to $a$, i.e., $\max(a, b) = a$.

max_eq_right_of_lt theorem

(h : a < b) : max a b = b

Full source

lemma max_eq_right_of_lt (h : a < b) : max a b = b := max_eq_right (le_of_lt h)

Maximum Identity for Strictly Ordered Elements: $\max(a, b) = b$ when $a < b$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, if $a < b$, then the maximum of $a$ and $b$ is equal to $b$, i.e., $\max(a, b) = b$.

lt_min theorem

(h₁ : a < b) (h₂ : a < c) : a < min b c

Full source

lemma lt_min (h₁ : a < b) (h₂ : a < c) : a < min b c := by
  cases le_total b c <;> simp [min_eq_left, min_eq_right, *]

Strict Inequality Preserved Under Minimum: $a < \min(b, c)$ when $a < b$ and $a < c$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered type $\alpha$, if $a < b$ and $a < c$, then $a$ is less than the minimum of $b$ and $c$, i.e., $a < \min(b, c)$.

max_lt theorem

(h₁ : a < c) (h₂ : b < c) : max a b < c

Full source

lemma max_lt (h₁ : a < c) (h₂ : b < c) : max a b < c := by
  cases le_total a b <;> simp [max_eq_left, max_eq_right, *]

Maximum of Two Elements Less Than a Third When Both Are Less Than It

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a < c$ and $b < c$, then the maximum of $a$ and $b$ is strictly less than $c$, i.e., $\max(a, b) < c$.

compare_lt_iff_lt theorem

: compare a b = .lt ↔ a < b

Full source

lemma compare_lt_iff_lt : comparecompare a b = .lt ↔ a < b := by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
  split_ifs <;> simp only [*, lt_irrefl, reduceCtorEq]

Comparison Yields Less-Than if and only if Strictly Less Than

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function `compare` returns `Ordering.lt` if and only if $a < b$. In other words, $\text{compare}(a, b) = \text{lt} \leftrightarrow a < b$.

compare_gt_iff_gt theorem

: compare a b = .gt ↔ a > b

Full source

lemma compare_gt_iff_gt : comparecompare a b = .gt ↔ a > b := by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
  split_ifs <;> simp only [*, lt_irrefl, not_lt_of_gt, reduceCtorEq]
  case _ h₁ h₂ =>
    have h : b < a := lt_trichotomy a b |>.resolve_left h₁ |>.resolve_left h₂
    rwa [true_iff]

Comparison Yields Greater-Than if and only if Strictly Greater Than

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function `compare` returns `Ordering.gt` if and only if $a > b$. In other words, $\text{compare}(a, b) = \text{gt} \leftrightarrow a > b$.

compare_eq_iff_eq theorem

: compare a b = .eq ↔ a = b

Full source

lemma compare_eq_iff_eq : comparecompare a b = .eq ↔ a = b := by
  rw [LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq]
  split_ifs <;> try simp only [reduceCtorEq]
  case _ h   => rw [false_iff]; exact ne_iff_lt_or_gt.2 <| .inl h
  case _ _ h => rwa [true_iff]
  case _ _ h => rwa [false_iff]

Comparison Yields Equal if and only if Elements Are Equal

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\text{compare}(a, b)$ returns $\text{eq}$ if and only if $a = b$.

compare_le_iff_le theorem

: compare a b ≠ .gt ↔ a ≤ b

Full source

lemma compare_le_iff_le : comparecompare a b ≠ .gtcompare a b ≠ .gt ↔ a ≤ b := by
  cases h : compare a b <;> simp
  · exact le_of_lt <| compare_lt_iff_lt.1 h
  · exact le_of_eq <| compare_eq_iff_eq.1 h
  · exact compare_gt_iff_gt.1 h

Comparison Does Not Yield Greater-Than if and only if Less Than or Equal To

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\text{compare}(a, b)$ does not return $\text{gt}$ if and only if $a \leq b$.

compare_ge_iff_ge theorem

: compare a b ≠ .lt ↔ a ≥ b

Full source

lemma compare_ge_iff_ge : comparecompare a b ≠ .ltcompare a b ≠ .lt ↔ a ≥ b := by
  cases h : compare a b <;> simp
  · exact compare_lt_iff_lt.1 h
  · exact le_of_eq <| (·.symm) <| compare_eq_iff_eq.1 h
  · exact le_of_lt <| compare_gt_iff_gt.1 h

Comparison Yields Not Less-Than if and only if Greater or Equal

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\text{compare}(a, b)$ does not return $\text{lt}$ if and only if $a \geq b$.

compare_iff theorem

(a b : α) {o : Ordering} : compare a b = o ↔ o.Compares a b

Full source

lemma compare_iff (a b : α) {o : Ordering} : comparecompare a b = o ↔ o.Compares a b := by
  cases o <;> simp only [Ordering.Compares]
  · exact compare_lt_iff_lt
  · exact compare_eq_iff_eq
  · exact compare_gt_iff_gt

Comparison Function Equivalence: $\text{compare}(a, b) = o \leftrightarrow o.\text{Compares}(a, b)$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$ and any ordering value $o$, the comparison function $\text{compare}(a, b)$ returns $o$ if and only if $o$ correctly relates $a$ and $b$ according to the linear order. That is, $\text{compare}(a, b) = o \leftrightarrow o.\text{Compares}(a, b)$.

cmp_eq_compare theorem

(a b : α) : cmp a b = compare a b

Full source

theorem cmp_eq_compare (a b : α) : cmp a b = compare a b := by
  refine ((compare_iff ..).2 ?_).symm
  unfold cmp cmpUsing; split_ifs with h1 h2
  · exact h1
  · exact h2
  · exact le_antisymm (not_lt.1 h2) (not_lt.1 h1)

Equivalence of Comparison Functions: $\text{cmp}(a, b) = \text{compare}(a, b)$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\text{cmp}(a, b)$ is equal to the standard comparison function $\text{compare}(a, b)$.

cmp_eq_compareOfLessAndEq theorem

(a b : α) : cmp a b = compareOfLessAndEq a b

Full source

theorem cmp_eq_compareOfLessAndEq (a b : α) : cmp a b = compareOfLessAndEq a b :=
  (cmp_eq_compare ..).trans (LinearOrder.compare_eq_compareOfLessAndEq ..)

Equivalence of Comparison Functions: $\text{cmp} = \text{compareOfLessAndEq}$

Informal description

For any two elements $a$ and $b$ in a linearly ordered type $\alpha$, the comparison function $\text{cmp}(a, b)$ is equal to the comparison function $\text{compareOfLessAndEq}(a, b)$.

instLawfulCmpCompare_mathlib instance

: Batteries.LawfulCmp (compare (α := α))

Full source

instance : Batteries.LawfulCmp (compare (α := α)) where
  symm a b := by
    cases h : compare a b <;>
    simp only [Ordering.swap] <;> symm
    · exact compare_gt_iff_gt.2 <| compare_lt_iff_lt.1 h
    · exact compare_eq_iff_eq.2 <| compare_eq_iff_eq.1 h |>.symm
    · exact compare_lt_iff_lt.2 <| compare_gt_iff_gt.1 h
  le_trans := fun h₁ h₂ ↦
    compare_le_iff_le.2 <| le_trans (compare_le_iff_le.1 h₁) (compare_le_iff_le.1 h₂)
  cmp_iff_beq := by simp [compare_eq_iff_eq]
  cmp_iff_lt := by simp [compare_lt_iff_lt]
  cmp_iff_le := by simp [compare_le_iff_le]

Lawful Comparison Function for Linear Orders

Informal description

For any linearly ordered type $\alpha$, the comparison function `compare` satisfies the properties of a lawful comparison function. This means it is consistent with the order relation on $\alpha$ and follows the expected behavior for equality and inequality comparisons.