Comparison #

This file provides basic results about orderings and comparison in linear orders.

Definitions #

cmp_le: An ordering from ≤.
ordering.compares: Turns an ordering into < and = propositions.
linear_order_of_compares: Constructs a linear_order instance from the fact that any two elements that are not one strictly less than the other either way are equal.

def cmp_le {α : Type u_1} [has_le α] [decidable_rel has_le.le] (x y : α) :

Like cmp, but uses a ≤ on the type instead of <. Given two elements x and y, returns a three-way comparison result ordering.

Equations

cmp_le x y = ite (x ≤ y) (ite (y ≤ x) ordering.eq ordering.lt) ordering.gt

source

theorem cmp_le_swap {α : Type u_1} [has_le α] [is_total α has_le.le] [decidable_rel has_le.le] (x y : α) :

(cmp_le x y).swap = cmp_le y x

source

theorem cmp_le_eq_cmp {α : Type u_1} [preorder α] [is_total α has_le.le] [decidable_rel has_le.le] [decidable_rel has_lt.lt] (x y : α) :

cmp_le x y = cmp x y

source

@[simp]

def ordering.compares {α : Type u_1} [has_lt α] :

ordering → α → α → Prop

compares o a b means that a and b have the ordering relation o between them, assuming that the relation a < b is defined.

Equations

ordering.gt.compares a b = (a > b)
ordering.eq.compares a b = (a = b)
ordering.lt.compares a b = (a < b)

source

theorem ordering.compares_swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

o.swap.compares a b ↔ o.compares b a

source

theorem ordering.compares.of_swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

o.swap.compares a b → o.compares b a

Alias of compares_swap.

source

theorem ordering.compares.swap {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

o.compares b a → o.swap.compares a b

Alias of compares_swap.

source

theorem ordering.swap_eq_iff_eq_swap {o o' : ordering} :

o.swap = o' ↔ o = o'.swap

source

theorem ordering.compares.eq_lt {α : Type u_1} [preorder α] {o : ordering} {a b : α} :

o.compares a b → (o = ordering.lt ↔ a < b)

source

theorem ordering.compares.ne_lt {α : Type u_1} [preorder α] {o : ordering} {a b : α} :

o.compares a b → (o ≠ ordering.lt ↔ b ≤ a)

source

theorem ordering.compares.eq_eq {α : Type u_1} [preorder α] {o : ordering} {a b : α} :

o.compares a b → (o = ordering.eq ↔ a = b)

source

theorem ordering.compares.eq_gt {α : Type u_1} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :

o = ordering.gt ↔ b < a

source

theorem ordering.compares.ne_gt {α : Type u_1} [preorder α] {o : ordering} {a b : α} (h : o.compares a b) :

o ≠ ordering.gt ↔ a ≤ b

source

theorem ordering.compares.le_total {α : Type u_1} [preorder α] {a b : α} {o : ordering} :

o.compares a b → a ≤ b ∨ b ≤ a

source

theorem ordering.compares.le_antisymm {α : Type u_1} [preorder α] {a b : α} {o : ordering} :

o.compares a b → a ≤ b → b ≤ a → a = b

source

theorem ordering.compares.inj {α : Type u_1} [preorder α] {o₁ o₂ : ordering} {a b : α} :

o₁.compares a b → o₂.compares a b → o₁ = o₂

source

theorem ordering.compares_iff_of_compares_impl {α : Type u_1} {β : Type u_2} [linear_order α] [preorder β] {a b : α} {a' b' : β} (h : ∀ {o : ordering}, o.compares a b → o.compares a' b') (o : ordering) :

o.compares a b ↔ o.compares a' b'

source

theorem ordering.swap_or_else (o₁ o₂ : ordering) :

(o₁.or_else o₂).swap = o₁.swap.or_else o₂.swap

source

theorem ordering.or_else_eq_lt (o₁ o₂ : ordering) :

o₁.or_else o₂ = ordering.lt ↔ o₁ = ordering.lt ∨ o₁ = ordering.eq ∧ o₂ = ordering.lt

source

theorem order_dual.dual_compares {α : Type u_1} [has_lt α] {a b : α} {o : ordering} :

o.compares a b ↔ o.compares b a

source

theorem cmp_compares {α : Type u_1} [linear_order α] (a b : α) :

(cmp a b).compares a b

source

theorem cmp_swap {α : Type u_1} [preorder α] [decidable_rel has_lt.lt] (a b : α) :

(cmp a b).swap = cmp b a

source

theorem order_dual.cmp_le_flip {α : Type u_1} [has_le α] [decidable_rel has_le.le] (x y : α) :

cmp_le x y = cmp_le y x

source

def linear_order_of_compares {α : Type u_1} [preorder α] (cmp : α → α → ordering) (h : ∀ (a b : α), (cmp a b).compares a b) :

linear_order α

Generate a linear order structure from a preorder and cmp function.

Equations

linear_order_of_compares cmp h = {le := preorder.le _inst_1, lt := preorder.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : α), decidable_of_iff (cmp a b ≠ ordering.gt) _, decidable_eq := λ (a b : α), decidable_of_iff (cmp a b = ordering.eq) _, decidable_lt := λ (a b : α), decidable_of_iff (cmp a b = ordering.lt) _, max := max_default (λ (a b : α), decidable_of_iff (cmp a b ≠ ordering.gt) _), max_def := _, min := min_default (λ (a b : α), decidable_of_iff (cmp a b ≠ ordering.gt) _), min_def := _}

source

@[simp]

theorem cmp_eq_lt_iff {α : Type u_1} [linear_order α] (x y : α) :

cmp x y = ordering.lt ↔ x < y

source

@[simp]

theorem cmp_eq_eq_iff {α : Type u_1} [linear_order α] (x y : α) :

cmp x y = ordering.eq ↔ x = y

source

@[simp]

theorem cmp_eq_gt_iff {α : Type u_1} [linear_order α] (x y : α) :

cmp x y = ordering.gt ↔ y < x

source

@[simp]

theorem cmp_self_eq_eq {α : Type u_1} [linear_order α] (x : α) :

cmp x x = ordering.eq

source

theorem cmp_eq_cmp_symm {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} :

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

source

theorem lt_iff_lt_of_cmp_eq_cmp {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :

x < y ↔ x' < y'

source

theorem le_iff_le_of_cmp_eq_cmp {α : Type u_1} [linear_order α] {x y : α} {β : Type u_2} [linear_order β] {x' y' : β} (h : cmp x y = cmp x' y') :

x ≤ y ↔ x' ≤ y'