Documentation

Mathlib.Order.Compare

Comparison #

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

Definitions #

def cmpLE {α : Type u_3} [LE α] [DecidableRel fun x x_1 => x x_1] (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
Instances For
    theorem cmpLE_swap {α : Type u_3} [LE α] [IsTotal α fun x x_1 => x x_1] [DecidableRel fun x x_1 => x x_1] (x : α) (y : α) :
    theorem cmpLE_eq_cmp {α : Type u_3} [Preorder α] [IsTotal α fun x x_1 => x x_1] [DecidableRel fun x x_1 => x x_1] [DecidableRel fun x x_1 => x < x_1] (x : α) (y : α) :
    cmpLE x y = cmp x y
    def Ordering.Compares {α : Type u_1} [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
    Instances For
      @[simp]
      theorem Ordering.compares_lt {α : Type u_1} [LT α] (a : α) (b : α) :
      @[simp]
      theorem Ordering.compares_eq {α : Type u_1} [LT α] (a : α) (b : α) :
      @[simp]
      theorem Ordering.compares_gt {α : Type u_1} [LT α] (a : α) (b : α) :
      theorem Ordering.compares_swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
      theorem Ordering.Compares.swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :

      Alias of the reverse direction of Ordering.compares_swap.

      theorem Ordering.Compares.of_swap {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :

      Alias of the forward direction of Ordering.compares_swap.

      theorem Ordering.Compares.eq_lt {α : Type u_1} [Preorder α] {o : Ordering} {a : α} {b : α} :
      Ordering.Compares o a b → (o = Ordering.lt a < b)
      theorem Ordering.Compares.ne_lt {α : Type u_1} [Preorder α] {o : Ordering} {a : α} {b : α} :
      theorem Ordering.Compares.eq_eq {α : Type u_1} [Preorder α] {o : Ordering} {a : α} {b : α} :
      Ordering.Compares o a b → (o = Ordering.eq a = b)
      theorem Ordering.Compares.eq_gt {α : Type u_1} [Preorder α] {o : Ordering} {a : α} {b : α} (h : Ordering.Compares o a b) :
      theorem Ordering.Compares.ne_gt {α : Type u_1} [Preorder α] {o : Ordering} {a : α} {b : α} (h : Ordering.Compares o a b) :
      theorem Ordering.Compares.le_total {α : Type u_1} [Preorder α] {a : α} {b : α} {o : Ordering} :
      Ordering.Compares o a ba b b a
      theorem Ordering.Compares.le_antisymm {α : Type u_1} [Preorder α] {a : α} {b : α} {o : Ordering} :
      Ordering.Compares o a ba bb aa = b
      theorem Ordering.Compares.inj {α : Type u_1} [Preorder α] {o₁ : Ordering} {o₂ : Ordering} {a : α} {b : α} :
      Ordering.Compares o₁ a bOrdering.Compares o₂ a bo₁ = o₂
      theorem Ordering.compares_iff_of_compares_impl {α : Type u_1} {β : Type u_2} [LinearOrder α] [Preorder β] {a : α} {b : α} {a' : β} {b' : β} (h : ∀ {o : Ordering}, Ordering.Compares o a bOrdering.Compares o a' b') (o : Ordering) :
      @[simp]
      theorem toDual_compares_toDual {α : Type u_1} [LT α] {a : α} {b : α} {o : Ordering} :
      Ordering.Compares o (OrderDual.toDual a) (OrderDual.toDual b) Ordering.Compares o b a
      @[simp]
      theorem ofDual_compares_ofDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} {o : Ordering} :
      Ordering.Compares o (OrderDual.ofDual a) (OrderDual.ofDual b) Ordering.Compares o b a
      theorem cmp_compares {α : Type u_1} [LinearOrder α] (a : α) (b : α) :
      theorem Ordering.Compares.cmp_eq {α : Type u_1} [LinearOrder α] {a : α} {b : α} {o : Ordering} (h : Ordering.Compares o a b) :
      cmp a b = o
      @[simp]
      theorem cmp_swap {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x < x_1] (a : α) (b : α) :
      @[simp]
      theorem cmpLE_toDual {α : Type u_1} [LE α] [DecidableRel fun x x_1 => x x_1] (x : α) (y : α) :
      cmpLE (OrderDual.toDual x) (OrderDual.toDual y) = cmpLE y x
      @[simp]
      theorem cmpLE_ofDual {α : Type u_1} [LE α] [DecidableRel fun x x_1 => x x_1] (x : αᵒᵈ) (y : αᵒᵈ) :
      cmpLE (OrderDual.ofDual x) (OrderDual.ofDual y) = cmpLE y x
      @[simp]
      theorem cmp_toDual {α : Type u_1} [LT α] [DecidableRel fun x x_1 => x < x_1] (x : α) (y : α) :
      cmp (OrderDual.toDual x) (OrderDual.toDual y) = cmp y x
      @[simp]
      theorem cmp_ofDual {α : Type u_1} [LT α] [DecidableRel fun x x_1 => x < x_1] (x : αᵒᵈ) (y : αᵒᵈ) :
      cmp (OrderDual.ofDual x) (OrderDual.ofDual y) = cmp y x
      def linearOrderOfCompares {α : Type u_1} [Preorder α] (cmp : ααOrdering) (h : ∀ (a b : α), Ordering.Compares (cmp a b) a b) :

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem cmp_eq_lt_iff {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
        @[simp]
        theorem cmp_eq_eq_iff {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
        @[simp]
        theorem cmp_eq_gt_iff {α : Type u_1} [LinearOrder α] (x : α) (y : α) :
        @[simp]
        theorem cmp_self_eq_eq {α : Type u_1} [LinearOrder α] (x : α) :
        theorem cmp_eq_cmp_symm {α : Type u_1} [LinearOrder α] {x : α} {y : α} {β : Type u_3} [LinearOrder β] {x' : β} {y' : β} :
        cmp x y = cmp x' y' cmp y x = cmp y' x'
        theorem lt_iff_lt_of_cmp_eq_cmp {α : Type u_1} [LinearOrder α] {x : α} {y : α} {β : Type u_3} [LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
        x < y x' < y'
        theorem le_iff_le_of_cmp_eq_cmp {α : Type u_1} [LinearOrder α] {x : α} {y : α} {β : Type u_3} [LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
        x y x' y'
        theorem eq_iff_eq_of_cmp_eq_cmp {α : Type u_1} [LinearOrder α] {x : α} {y : α} {β : Type u_3} [LinearOrder β] {x' : β} {y' : β} (h : cmp x y = cmp x' y') :
        x = y x' = y'
        theorem LT.lt.cmp_eq_lt {α : Type u_1} [LinearOrder α] {x : α} {y : α} (h : x < y) :
        theorem LT.lt.cmp_eq_gt {α : Type u_1} [LinearOrder α] {x : α} {y : α} (h : x < y) :
        theorem Eq.cmp_eq_eq {α : Type u_1} [LinearOrder α] {x : α} {y : α} (h : x = y) :
        theorem Eq.cmp_eq_eq' {α : Type u_1} [LinearOrder α] {x : α} {y : α} (h : x = y) :