Documentation

Mathlib.Order.Compare

Comparison #

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

Definitions #

def cmpLE {α : Type u_3} [LE α] [DecidableLE α] (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 (x1 x2 : α) => x1 x2] [DecidableLE α] (x y : α) :
      (cmpLE x y).swap = cmpLE y x
      theorem cmpLE_eq_cmp {α : Type u_3} [Preorder α] [IsTotal α fun (x1 x2 : α) => x1 x2] [DecidableLE α] [DecidableLT α] (x y : α) :
      cmpLE x y = cmp x y
      theorem Ordering.compares_swap {α : Type u_1} [LT α] {a b : α} {o : Ordering} :
      theorem Ordering.Compares.of_swap {α : Type u_1} [LT α] {a b : α} {o : Ordering} :
      o.swap.Compares a bo.Compares b a

      Alias of the forward direction of Ordering.compares_swap.

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

      Alias of the reverse direction of Ordering.compares_swap.

      theorem Ordering.Compares.eq_lt {α : Type u_1} [Preorder α] {o : Ordering} {a b : α} :
      o.Compares a b → (o = lt a < b)
      theorem Ordering.Compares.ne_lt {α : Type u_1} [Preorder α] {o : Ordering} {a b : α} :
      o.Compares a b → (o lt b a)
      theorem Ordering.Compares.eq_eq {α : Type u_1} [Preorder α] {o : Ordering} {a b : α} :
      o.Compares a b → (o = eq a = b)
      theorem Ordering.Compares.eq_gt {α : Type u_1} [Preorder α] {o : Ordering} {a b : α} (h : o.Compares a b) :
      o = gt b < a
      theorem Ordering.Compares.ne_gt {α : Type u_1} [Preorder α] {o : Ordering} {a b : α} (h : o.Compares a b) :
      o gt a b
      theorem Ordering.Compares.le_total {α : Type u_1} [Preorder α] {a b : α} {o : Ordering} :
      o.Compares a ba b b a
      theorem Ordering.Compares.le_antisymm {α : Type u_1} [Preorder α] {a b : α} {o : Ordering} :
      o.Compares a ba bb aa = b
      theorem Ordering.Compares.inj {α : Type u_1} [Preorder α] {o₁ o₂ : Ordering} {a b : α} :
      o₁.Compares a bo₂.Compares 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}, o.Compares a bo.Compares a' b') (o : Ordering) :
      o.Compares a b o.Compares a' b'
      @[simp]
      theorem toDual_compares_toDual {α : Type u_1} [LT α] {a b : α} {o : Ordering} :
      @[simp]
      theorem ofDual_compares_ofDual {α : Type u_1} [LT α] {a b : αᵒᵈ} {o : Ordering} :
      theorem cmp_compares {α : Type u_1} [LinearOrder α] (a b : α) :
      (cmp a b).Compares a b
      theorem Ordering.Compares.cmp_eq {α : Type u_1} [LinearOrder α] {a b : α} {o : Ordering} (h : o.Compares a b) :
      cmp a b = o
      @[simp]
      theorem cmp_swap {α : Type u_1} [Preorder α] [DecidableLT α] (a b : α) :
      (cmp a b).swap = cmp b a
      @[simp]
      theorem cmpLE_toDual {α : Type u_1} [LE α] [DecidableLE α] (x y : α) :
      @[simp]
      theorem cmpLE_ofDual {α : Type u_1} [LE α] [DecidableLE α] (x y : αᵒᵈ) :
      @[simp]
      theorem cmp_toDual {α : Type u_1} [LT α] [DecidableLT α] (x y : α) :
      @[simp]
      theorem cmp_ofDual {α : Type u_1} [LT α] [DecidableLT α] (x y : αᵒᵈ) :
      def linearOrderOfCompares {α : Type u_1} [Preorder α] (cmp : ααOrdering) (h : ∀ (a b : α), (cmp a b).Compares a b) :

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

      Equations
        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) :