Documentation

Mathlib.Order.Basic

Basic definitions about and < #

This file proves basic results about orders, provides extensive dot notation, defines useful order classes and allows to transfer order instances.

Type synonyms #

Transferring orders #

Extra class #

Notes #

and < are highly favored over and > in mathlib. The reason is that we can formulate all lemmas using /<, and rw has trouble unifying and . Hence choosing one direction spares us useless duplication. This is enforced by a linter. See Note [nolint_ge] for more infos.

Dot notation is particularly useful on (LE.le) and < (LT.lt). To that end, we provide many aliases to dot notation-less lemmas. For example, le_trans is aliased with LE.le.trans and can be used to construct hab.trans hbc : a ≤ c when hab : a ≤ b, hbc : b ≤ c, lt_of_le_of_lt is aliased as LE.le.trans_lt and can be used to construct hab.trans hbc : a < c when hab : a ≤ b, hbc : b < c.

TODO #

Tags #

preorder, order, partial order, poset, linear order, chain

Bare relations #

theorem LE.ext {α : Type u} {x y : LE α} (le : le = le) :
x = y
theorem LE.ext_iff {α : Type u} {x y : LE α} :
x = y le = le
theorem LE.le.ge {α : Type u_2} [LE α] {x y : α} (h : x y) :
y x
theorem GE.ge.le {α : Type u_2} [LE α] {x y : α} (h : x y) :
y x
theorem LT.lt.gt {α : Type u_2} [LT α] {x y : α} (h : x < y) :
y > x
theorem GT.gt.lt {α : Type u_2} [LT α] {x y : α} (h : x > y) :
y < x
def Order.Preimage {α : Type u_2} {β : Type u_3} (f : αβ) (s : ββProp) (x y : α) :

Given a relation R on β and a function f : α → β, the preimage relation on α is defined by x ≤ y ↔ f x ≤ f y. It is the unique relation on α making f a RelEmbedding (assuming f is injective).

Equations
    Instances For

      Given a relation R on β and a function f : α → β, the preimage relation on α is defined by x ≤ y ↔ f x ≤ f y. It is the unique relation on α making f a RelEmbedding (assuming f is injective).

      Equations
        Instances For
          instance Order.Preimage.decidable {α : Type u_2} {β : Type u_3} (f : αβ) (s : ββProp) [H : DecidableRel s] :

          The preimage of a decidable order is decidable.

          Equations

            Preorders #

            theorem le_trans' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca ba c
            theorem lt_trans' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca < ba < c
            theorem lt_of_le_of_lt' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca < ba < c
            theorem lt_of_lt_of_le' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca ba < c
            theorem le_of_le_of_eq' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca = ba c
            theorem le_of_eq_of_le' {α : Type u_2} [Preorder α] {a b c : α} :
            b = ca ba c
            theorem lt_of_lt_of_eq' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca = ba < c
            theorem lt_of_eq_of_lt' {α : Type u_2} [Preorder α] {a b c : α} :
            b = ca < ba < c
            theorem not_lt_iff_not_le_or_ge {α : Type u_2} [Preorder α] {a b : α} :
            ¬a < b ¬a b b a
            theorem not_lt_iff_le_imp_le {α : Type u_2} [Preorder α] {a b : α} :
            ¬a < b a bb a
            theorem ge_of_eq {α : Type u_2} [Preorder α] {a b : α} (h : a = b) :
            b a

            If x = y then y ≤ x. Note: this lemma uses y ≤ x instead of x ≥ y, because le is used almost exclusively in mathlib.

            @[simp]
            theorem lt_self_iff_false {α : Type u_2} [Preorder α] (x : α) :
            x < x False
            theorem LE.le.trans {α : Type u_1} [Preorder α] {a b c : α} :
            a bb ca c

            Alias of le_trans.


            The relation on a preorder is transitive.

            theorem LE.le.trans' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca ba c

            Alias of le_trans'.

            theorem LT.lt.trans {α : Type u_1} [Preorder α] {a b c : α} (hab : a < b) (hbc : b < c) :
            a < c

            Alias of lt_trans.

            theorem LT.lt.trans' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca < ba < c

            Alias of lt_trans'.

            theorem LE.le.trans_lt {α : Type u_1} [Preorder α] {a b c : α} (hab : a b) (hbc : b < c) :
            a < c

            Alias of lt_of_le_of_lt.

            theorem LE.le.trans_lt' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca < ba < c

            Alias of lt_of_le_of_lt'.

            theorem LT.lt.trans_le {α : Type u_1} [Preorder α] {a b c : α} (hab : a < b) (hbc : b c) :
            a < c

            Alias of lt_of_lt_of_le.

            theorem LT.lt.trans_le' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca ba < c

            Alias of lt_of_lt_of_le'.

            theorem LE.le.trans_eq {α : Type u_1} {a b c : α} [LE α] (h₁ : a b) (h₂ : b = c) :
            a c

            Alias of le_of_le_of_eq.

            theorem LE.le.trans_eq' {α : Type u_2} [Preorder α] {a b c : α} :
            b ca = ba c

            Alias of le_of_le_of_eq'.

            theorem LT.lt.trans_eq {α : Type u_1} {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) :
            a < c

            Alias of lt_of_lt_of_eq.

            theorem LT.lt.trans_eq' {α : Type u_2} [Preorder α] {a b c : α} :
            b < ca = ba < c

            Alias of lt_of_lt_of_eq'.

            theorem Eq.trans_le {α : Type u_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : b c) :
            a c

            Alias of le_of_eq_of_le.

            theorem Eq.trans_ge {α : Type u_2} [Preorder α] {a b c : α} :
            b = ca ba c

            Alias of le_of_eq_of_le'.

            theorem Eq.trans_lt {α : Type u_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) :
            a < c

            Alias of lt_of_eq_of_lt.

            theorem Eq.trans_gt {α : Type u_2} [Preorder α] {a b c : α} :
            b = ca < ba < c

            Alias of lt_of_eq_of_lt'.

            theorem LE.le.lt_of_not_le {α : Type u_1} [Preorder α] {a b : α} (hab : a b) (hba : ¬b a) :
            a < b

            Alias of lt_of_le_not_le.

            theorem LE.le.lt_or_eq_dec {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a b) :
            a < b a = b

            Alias of Decidable.lt_or_eq_of_le.

            theorem LT.lt.le {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) :
            a b

            Alias of le_of_lt.

            theorem LT.lt.ne {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
            a b

            Alias of ne_of_lt.

            theorem Eq.le {α : Type u_1} [Preorder α] {a b : α} (hab : a = b) :
            a b

            Alias of le_of_eq.

            theorem Eq.ge {α : Type u_2} [Preorder α] {a b : α} (h : a = b) :
            b a

            If x = y then y ≤ x. Note: this lemma uses y ≤ x instead of x ≥ y, because le is used almost exclusively in mathlib.

            theorem LT.lt.asymm {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
            ¬b < a

            Alias of lt_asymm.

            theorem LT.lt.not_lt {α : Type u_1} [Preorder α] {a b : α} (h : a < b) :
            ¬b < a

            Alias of lt_asymm.

            theorem ne_of_not_le {α : Type u_2} [Preorder α] {a b : α} (h : ¬a b) :
            a b
            theorem Eq.not_lt {α : Type u_2} [Preorder α] {a b : α} (hab : a = b) :
            ¬a < b
            theorem Eq.not_gt {α : Type u_2} [Preorder α] {a b : α} (hab : a = b) :
            ¬b < a
            @[simp]
            theorem le_of_subsingleton {α : Type u_2} [Preorder α] {a b : α} [Subsingleton α] :
            a b
            theorem not_lt_of_subsingleton {α : Type u_2} [Preorder α] {a b : α} [Subsingleton α] :
            ¬a < b
            theorem LT.lt.false {α : Type u_2} [Preorder α] {a : α} :
            a < aFalse
            theorem LT.lt.ne' {α : Type u_2} [Preorder α] {a b : α} (h : a < b) :
            b a
            theorem le_of_forall_le {α : Type u_2} [Preorder α] {a b : α} (H : ∀ (c : α), c ac b) :
            a b
            theorem le_of_forall_ge {α : Type u_2} [Preorder α] {a b : α} (H : ∀ (c : α), a cb c) :
            b a
            @[deprecated le_of_forall_ge (since := "2025-01-30")]
            theorem le_of_forall_le' {α : Type u_2} [Preorder α] {a b : α} (H : ∀ (c : α), a cb c) :
            b a

            Alias of le_of_forall_ge.

            theorem forall_le_iff_le {α : Type u_2} [Preorder α] {a b : α} :
            (∀ ⦃c : α⦄, c ac b) a b
            theorem forall_le_iff_ge {α : Type u_2} [Preorder α] {a b : α} :
            (∀ ⦃c : α⦄, a cb c) b a
            theorem le_implies_le_of_le_of_le {α : Type u_2} [Preorder α] {a b c d : α} (hca : c a) (hbd : b d) :
            a bc d

            monotonicity of with respect to

            Partial order #

            theorem ge_antisymm {α : Type u_2} [PartialOrder α] {a b : α} :
            a bb ab = a
            theorem lt_of_le_of_ne' {α : Type u_2} [PartialOrder α] {a b : α} :
            a bb aa < b
            theorem Ne.lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} :
            a ba ba < b
            theorem Ne.lt_of_le' {α : Type u_2} [PartialOrder α] {a b : α} :
            b aa ba < b
            theorem LE.le.antisymm {α : Type u_1} [PartialOrder α] {a b : α} :
            a bb aa = b

            Alias of le_antisymm.

            theorem LE.le.antisymm' {α : Type u_2} [PartialOrder α] {a b : α} :
            a bb ab = a

            Alias of ge_antisymm.

            theorem LE.le.lt_of_ne {α : Type u_1} [PartialOrder α] {a b : α} :
            a ba ba < b

            Alias of lt_of_le_of_ne.

            theorem LE.le.lt_of_ne' {α : Type u_2} [PartialOrder α] {a b : α} :
            a bb aa < b

            Alias of lt_of_le_of_ne'.

            theorem LE.le.lt_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
            a ba < b a = b

            Alias of lt_or_eq_of_le.

            theorem le_imp_eq_iff_le_imp_le {α : Type u_2} [PartialOrder α] {a b : α} :
            a bb = a a bb a
            theorem ge_imp_eq_iff_le_imp_le {α : Type u_2} [PartialOrder α] {a b : α} :
            a ba = b a bb a
            theorem LE.le.lt_iff_ne {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a < b a b
            theorem LE.le.gt_iff_ne {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a < b b a
            theorem LE.le.not_lt_iff_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            ¬a < b a = b
            theorem LE.le.not_gt_iff_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            ¬a < b b = a
            theorem LE.le.le_iff_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            b a b = a
            theorem LE.le.ge_iff_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            b a a = b
            theorem Decidable.le_iff_eq_or_lt {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] :
            a b a = b a < b
            theorem le_iff_eq_or_lt {α : Type u_2} [PartialOrder α] {a b : α} :
            a b a = b a < b
            theorem lt_iff_le_and_ne {α : Type u_2} [PartialOrder α] {a b : α} :
            a < b a b a b
            theorem eq_iff_not_lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) :
            a = b ¬a < b
            theorem LE.le.eq_iff_not_lt {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) :
            a = b ¬a < b

            Alias of eq_iff_not_lt_of_le.

            theorem Decidable.eq_iff_le_not_lt {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] :
            a = b a b ¬a < b
            theorem eq_iff_le_not_lt {α : Type u_2} [PartialOrder α] {a b : α} :
            a = b a b ¬a < b
            theorem eq_or_lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a = b a < b
            theorem eq_or_gt_of_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            b = a a < b
            theorem gt_or_eq_of_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a < b b = a
            theorem LE.le.eq_or_lt_dec {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : a b) :
            a = b a < b

            Alias of Decidable.eq_or_lt_of_le.

            theorem LE.le.eq_or_lt {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a = b a < b

            Alias of eq_or_lt_of_le.

            theorem LE.le.eq_or_gt {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            b = a a < b

            Alias of eq_or_gt_of_le.

            theorem LE.le.gt_or_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a < b b = a

            Alias of gt_or_eq_of_le.

            theorem eq_of_le_of_not_lt {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) (hba : ¬a < b) :
            a = b
            theorem eq_of_ge_of_not_gt {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) (hba : ¬a < b) :
            b = a
            theorem LE.le.eq_of_not_lt {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) (hba : ¬a < b) :
            a = b

            Alias of eq_of_le_of_not_lt.

            theorem LE.le.eq_of_not_gt {α : Type u_2} [PartialOrder α] {a b : α} (hab : a b) (hba : ¬a < b) :
            b = a

            Alias of eq_of_ge_of_not_gt.

            theorem Ne.le_iff_lt {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            a b a < b
            theorem Ne.not_le_or_not_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a b) :
            ¬a b ¬b a
            theorem Decidable.ne_iff_lt_iff_le {α : Type u_2} [PartialOrder α] {a b : α} [DecidableEq α] :
            (a b a < b) a b
            @[simp]
            theorem ne_iff_lt_iff_le {α : Type u_2} [PartialOrder α] {a b : α} :
            (a b a < b) a b
            theorem eq_of_forall_le_iff {α : Type u_2} [PartialOrder α] {a b : α} (H : ∀ (c : α), c a c b) :
            a = b
            theorem eq_of_forall_ge_iff {α : Type u_2} [PartialOrder α] {a b : α} (H : ∀ (c : α), a c b c) :
            a = b
            theorem commutative_of_le {α : Type u_2} {β : Type u_3} [PartialOrder α] {f : ββα} (comm : ∀ (a b : β), f a b f b a) (a b : β) :
            f a b = f b a

            To prove commutativity of a binary operation , we only to check a ○ b ≤ b ○ a for all a, b.

            theorem associative_of_commutative_of_le {α : Type u_2} [PartialOrder α] {f : ααα} (comm : Std.Commutative f) (assoc : ∀ (a b c : α), f (f a b) c f a (f b c)) :

            To prove associativity of a commutative binary operation , we only to check (a ○ b) ○ c ≤ a ○ (b ○ c) for all a, b, c.

            theorem LE.le.lt_or_le {α : Type u_2} [LinearOrder α] {a b : α} (h : a b) (c : α) :
            a < c c b
            theorem LE.le.le_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a b) (c : α) :
            a c c < b
            theorem LE.le.le_or_le {α : Type u_2} [LinearOrder α] {a b : α} (h : a b) (c : α) :
            a c c b
            theorem LT.lt.lt_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a < b) (c : α) :
            a < c c < b
            theorem min_def' {α : Type u_2} [LinearOrder α] (a b : α) :
            min a b = if b a then b else a
            theorem max_def' {α : Type u_2} [LinearOrder α] (a b : α) :
            max a b = if b a then a else b
            theorem lt_of_not_le {α : Type u_2} [LinearOrder α] {a b : α} (h : ¬b a) :
            a < b
            theorem lt_iff_not_le {α : Type u_2} [LinearOrder α] {a b : α} :
            a < b ¬b a
            theorem Ne.lt_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a b) :
            a < b b < a
            @[simp]
            theorem lt_or_lt_iff_ne {α : Type u_2} [LinearOrder α] {a b : α} :
            a < b b < a a b

            A version of ne_iff_lt_or_gt with LHS and RHS reversed.

            theorem not_lt_iff_eq_or_lt {α : Type u_2} [LinearOrder α] {a b : α} :
            ¬a < b a = b b < a
            theorem exists_ge_of_linear {α : Type u_2} [LinearOrder α] (a b : α) :
            (c : α), a c b c
            theorem exists_forall_ge_and {α : Type u_2} [LinearOrder α] {p q : αProp} :
            ( (i : α), ∀ (j : α), j ip j) → ( (i : α), ∀ (j : α), j iq j) → (i : α), ∀ (j : α), j ip j q j
            theorem le_of_forall_lt {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), c < ac < b) :
            a b
            theorem forall_lt_iff_le {α : Type u_2} [LinearOrder α] {a b : α} :
            (∀ ⦃c : α⦄, c < ac < b) a b
            theorem le_of_forall_lt' {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), a < cb < c) :
            b a
            theorem forall_lt_iff_le' {α : Type u_2} [LinearOrder α] {a b : α} :
            (∀ ⦃c : α⦄, a < cb < c) b a
            theorem eq_of_forall_lt_iff {α : Type u_2} [LinearOrder α] {a b : α} (h : ∀ (c : α), c < a c < b) :
            a = b
            theorem eq_of_forall_gt_iff {α : Type u_2} [LinearOrder α] {a b : α} (h : ∀ (c : α), a < c b < c) :
            a = b
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : x < y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
            ltByCases x y h₁ h₂ h₃ = h₁ h
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_gt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : y < x) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
            ltByCases x y h₁ h₂ h₃ = h₃ h
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_eq {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : x = y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
            ltByCases x y h₁ h₂ h₃ = h₂ h
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_not_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : ¬x < y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : ¬y < xx = y := ) :
            ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_not_gt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : ¬y < x) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : ¬x < yx = y := ) :
            ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_ne {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} (h : x y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : ¬x < yy < x := ) :
            ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_comm {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : y = xx = y := ) :
            ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ p) h₁
            theorem eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt {α : Type u_2} [LinearOrder α] {x y x' y' : α} (ltc : x < y x' < y') (gtc : y < x y' < x') :
            x = y x' = y'
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_rec {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : P) (hlt : ∀ (h : x < y), h₁ h = p) (heq : ∀ (h : x = y), h₂ h = p) (hgt : ∀ (h : y < x), h₃ h = p) :
            ltByCases x y h₁ h₂ h₃ = p
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_eq_iff {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} {p : P} :
            ltByCases x y h₁ h₂ h₃ = p ( (h : x < y), h₁ h = p) ( (h : x = y), h₂ h = p) (h : y < x), h₃ h = p
            @[deprecated lt_trichotomy (since := "2025-04-21")]
            theorem ltByCases_congr {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y x' y' : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} {h₁' : x' < y'P} {h₂' : x' = y'P} {h₃' : y' < x'P} (ltc : x < y x' < y') (gtc : y < x y' < x') (hh'₁ : ∀ (h : x' < y'), h₁ = h₁' h) (hh'₂ : ∀ (h : x' = y'), h₂ = h₂' h) (hh'₃ : ∀ (h : y' < x'), h₃ = h₃' h) :
            ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃'
            @[reducible, inline, deprecated lt_trichotomy (since := "2025-04-21")]
            abbrev ltTrichotomy {α : Type u_2} [LinearOrder α] {P : Sort u_5} (x y : α) (p q r : P) :
            P

            Perform a case-split on the ordering of x and y in a decidable linear order, non-dependently.

            Equations
              Instances For
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : x < y) :
                ltTrichotomy x y p q r = p
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_gt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : y < x) :
                ltTrichotomy x y p q r = r
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_eq {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : x = y) :
                ltTrichotomy x y p q r = q
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_not_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : ¬x < y) :
                ltTrichotomy x y p q r = if y < x then r else q
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_not_gt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : ¬y < x) :
                ltTrichotomy x y p q r = if x < y then p else q
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_ne {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} (h : x y) :
                ltTrichotomy x y p q r = if x < y then p else r
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_comm {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} :
                ltTrichotomy x y p q r = ltTrichotomy y x r q p
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_self {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p : P} :
                ltTrichotomy x y p p p = p
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_eq_iff {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r s : P} :
                ltTrichotomy x y p q r = s x < y p = s x = y q = s y < x r = s
                @[deprecated lt_trichotomy (since := "2025-04-21")]
                theorem ltTrichotomy_congr {α : Type u_2} [LinearOrder α] {P : Sort u_5} {x y : α} {p q r : P} {x' y' : α} {p' q' r' : P} (ltc : x < y x' < y') (gtc : y < x y' < x') (hh'₁ : x' < y'p = p') (hh'₂ : x' = y'q = q') (hh'₃ : y' < x'r = r') :
                ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r'

                min/max recursors #

                theorem min_rec {α : Type u_2} [LinearOrder α] {a b : α} {p : αProp} (ha : a bp a) (hb : b ap b) :
                p (min a b)
                theorem max_rec {α : Type u_2} [LinearOrder α] {a b : α} {p : αProp} (ha : b ap a) (hb : a bp b) :
                p (max a b)
                theorem min_rec' {α : Type u_2} [LinearOrder α] {a b : α} (p : αProp) (ha : p a) (hb : p b) :
                p (min a b)
                theorem max_rec' {α : Type u_2} [LinearOrder α] {a b : α} (p : αProp) (ha : p a) (hb : p b) :
                p (max a b)
                theorem min_def_lt {α : Type u_2} [LinearOrder α] (a b : α) :
                min a b = if a < b then a else b
                theorem max_def_lt {α : Type u_2} [LinearOrder α] (a b : α) :
                max a b = if a < b then b else a

                Implications #

                theorem lt_imp_lt_of_le_imp_le {α : Type u_2} {β : Type u_5} [LinearOrder α] [Preorder β] {a b : α} {c d : β} (H : a bc d) (h : d < c) :
                b < a
                theorem le_imp_le_iff_lt_imp_lt {α : Type u_2} {β : Type u_5} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
                a bc d d < cb < a
                theorem lt_iff_lt_of_le_iff_le' {α : Type u_2} {β : Type u_5} [Preorder α] [Preorder β] {a b : α} {c d : β} (H : a b c d) (H' : b a d c) :
                b < a d < c
                theorem lt_iff_lt_of_le_iff_le {α : Type u_2} {β : Type u_5} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} (H : a b c d) :
                b < a d < c
                theorem le_iff_le_iff_lt_iff_lt {α : Type u_2} {β : Type u_5} [LinearOrder α] [LinearOrder β] {a b : α} {c d : β} :
                (a b c d) (b < a d < c)
                theorem rel_imp_eq_of_rel_imp_le {α : Type u_2} {β : Type u_3} [PartialOrder β] (r : ααProp) [IsSymm α r] {f : αβ} (h : ∀ (a b : α), r a bf a f b) {a b : α} :
                r a bf a = f b

                A symmetric relation implies two values are equal, when it implies they're less-equal.

                Extensionality lemmas #

                theorem Preorder.toLE_injective_iff {α : Type u_2} {a₁ a₂ : Preorder α} :
                a₁ = a₂ a₁.toLE = a₂.toLE
                theorem PartialOrder.toPreorder_injective_iff {α : Type u_2} {a₁ a₂ : PartialOrder α} :
                a₁ = a₂ a₁.toPreorder = a₂.toPreorder
                theorem LinearOrder.toPartialOrder_injective_iff {α : Type u_2} {a₁ a₂ : LinearOrder α} :
                a₁ = a₂ a₁.toPartialOrder = a₂.toPartialOrder
                theorem Preorder.ext {α : Type u_2} {A B : Preorder α} (H : ∀ (x y : α), x y x y) :
                A = B
                theorem PartialOrder.ext {α : Type u_2} {A B : PartialOrder α} (H : ∀ (x y : α), x y x y) :
                A = B
                theorem PartialOrder.ext_lt {α : Type u_2} {A B : PartialOrder α} (H : ∀ (x y : α), x < y x < y) :
                A = B
                theorem LinearOrder.ext {α : Type u_2} {A B : LinearOrder α} (H : ∀ (x y : α), x y x y) :
                A = B
                theorem LinearOrder.ext_lt {α : Type u_2} {A B : LinearOrder α} (H : ∀ (x y : α), x < y x < y) :
                A = B

                Order dual #

                def OrderDual (α : Type u_5) :
                Type u_5

                Type synonym to equip a type with the dual order: means and < means >. αᵒᵈ is notation for OrderDual α.

                Equations
                  Instances For

                    Type synonym to equip a type with the dual order: means and < means >. αᵒᵈ is notation for OrderDual α.

                    Equations
                      Instances For
                        instance OrderDual.instNonempty (α : Type u_5) [h : Nonempty α] :
                        instance OrderDual.instLE (α : Type u_5) [LE α] :
                        Equations
                          instance OrderDual.instLT (α : Type u_5) [LT α] :
                          Equations
                            instance OrderDual.instOrd (α : Type u_5) [Ord α] :
                            Equations
                              instance OrderDual.instSup (α : Type u_5) [Min α] :
                              Equations
                                instance OrderDual.instInf (α : Type u_5) [Max α] :
                                Equations
                                  instance OrderDual.instPreorder (α : Type u_5) [Preorder α] :
                                  Equations
                                    def LinearOrder.swap (α : Type u_5) :

                                    The opposite linear order to a given linear order

                                    Equations
                                      Instances For
                                        Equations
                                          theorem OrderDual.Ord.dual_dual (α : Type u_5) [H : Ord α] :

                                          HasCompl #

                                          Equations
                                            instance Pi.hasCompl {ι : Type u_1} {π : ιType u_4} [(i : ι) → HasCompl (π i)] :
                                            HasCompl ((i : ι) → π i)
                                            Equations
                                              theorem Pi.compl_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → HasCompl (π i)] (x : (i : ι) → π i) :
                                              x = fun (i : ι) => (x i)
                                              @[simp]
                                              theorem Pi.compl_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → HasCompl (π i)] (x : (i : ι) → π i) (i : ι) :
                                              x i = (x i)
                                              instance IsIrrefl.compl {α : Type u_2} (r : ααProp) [IsIrrefl α r] :
                                              instance IsRefl.compl {α : Type u_2} (r : ααProp) [IsRefl α r] :
                                              theorem compl_lt {α : Type u_2} [LinearOrder α] :
                                              (fun (x1 x2 : α) => x1 < x2) = fun (x1 x2 : α) => x1 x2
                                              theorem compl_le {α : Type u_2} [LinearOrder α] :
                                              (fun (x1 x2 : α) => x1 x2) = fun (x1 x2 : α) => x1 > x2
                                              theorem compl_gt {α : Type u_2} [LinearOrder α] :
                                              (fun (x1 x2 : α) => x1 > x2) = fun (x1 x2 : α) => x1 x2
                                              theorem compl_ge {α : Type u_2} [LinearOrder α] :
                                              (fun (x1 x2 : α) => x1 x2) = fun (x1 x2 : α) => x1 < x2
                                              instance Ne.instIsEquiv_compl {α : Type u_2} :
                                              IsEquiv α (fun (x1 x2 : α) => x1 x2)

                                              Order instances on the function space #

                                              instance Pi.hasLe {ι : Type u_1} {π : ιType u_4} [(i : ι) → LE (π i)] :
                                              LE ((i : ι) → π i)
                                              Equations
                                                theorem Pi.le_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → LE (π i)] {x y : (i : ι) → π i} :
                                                x y ∀ (i : ι), x i y i
                                                instance Pi.preorder {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] :
                                                Preorder ((i : ι) → π i)
                                                Equations
                                                  theorem Pi.lt_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {x y : (i : ι) → π i} :
                                                  x < y x y (i : ι), x i < y i
                                                  instance Pi.partialOrder {ι : Type u_1} {π : ιType u_4} [(i : ι) → PartialOrder (π i)] :
                                                  PartialOrder ((i : ι) → π i)
                                                  Equations
                                                    @[simp]
                                                    theorem Sum.elim_le_elim_iff {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [LE β] {u₁ v₁ : α₁β} {u₂ v₂ : α₂β} :
                                                    Sum.elim u₁ u₂ Sum.elim v₁ v₂ u₁ v₁ u₂ v₂
                                                    theorem Sum.const_le_elim_iff {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [LE β] {b : β} {v₁ : α₁β} {v₂ : α₂β} :
                                                    Function.const (α₁ α₂) b Sum.elim v₁ v₂ Function.const α₁ b v₁ Function.const α₂ b v₂
                                                    theorem Sum.elim_le_const_iff {β : Type u_3} {α₁ : Type u_5} {α₂ : Type u_6} [LE β] {b : β} {u₁ : α₁β} {u₂ : α₂β} :
                                                    Sum.elim u₁ u₂ Function.const (α₁ α₂) b u₁ Function.const α₁ b u₂ Function.const α₂ b
                                                    def StrongLT {ι : Type u_1} {π : ιType u_4} [(i : ι) → LT (π i)] (a b : (i : ι) → π i) :

                                                    A function a is strongly less than a function b if a i < b i for all i.

                                                    Equations
                                                      Instances For
                                                        theorem le_of_strongLT {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b : (i : ι) → π i} (h : StrongLT a b) :
                                                        a b
                                                        theorem lt_of_strongLT {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b : (i : ι) → π i} [Nonempty ι] (h : StrongLT a b) :
                                                        a < b
                                                        theorem strongLT_of_strongLT_of_le {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b c : (i : ι) → π i} (hab : StrongLT a b) (hbc : b c) :
                                                        theorem strongLT_of_le_of_strongLT {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b c : (i : ι) → π i} (hab : a b) (hbc : StrongLT b c) :
                                                        theorem StrongLT.le {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b : (i : ι) → π i} (h : StrongLT a b) :
                                                        a b

                                                        Alias of le_of_strongLT.

                                                        theorem StrongLT.lt {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b : (i : ι) → π i} [Nonempty ι] (h : StrongLT a b) :
                                                        a < b

                                                        Alias of lt_of_strongLT.

                                                        theorem StrongLT.trans_le {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b c : (i : ι) → π i} (hab : StrongLT a b) (hbc : b c) :

                                                        Alias of strongLT_of_strongLT_of_le.

                                                        theorem LE.le.trans_strongLT {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] {a b c : (i : ι) → π i} (hab : a b) (hbc : StrongLT b c) :

                                                        Alias of strongLT_of_le_of_strongLT.

                                                        theorem le_update_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x y : (i : ι) → π i} {i : ι} {a : π i} :
                                                        x Function.update y i a x i a ∀ (j : ι), j ix j y j
                                                        theorem update_le_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x y : (i : ι) → π i} {i : ι} {a : π i} :
                                                        Function.update x i a y a y i ∀ (j : ι), j ix j y j
                                                        theorem update_le_update_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x y : (i : ι) → π i} {i : ι} {a b : π i} :
                                                        Function.update x i a Function.update y i b a b ∀ (j : ι), j ix j y j
                                                        @[simp]
                                                        theorem update_le_update_iff' {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a b : π i} :
                                                        @[simp]
                                                        theorem update_lt_update_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a b : π i} :
                                                        @[simp]
                                                        theorem le_update_self_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
                                                        x Function.update x i a x i a
                                                        @[simp]
                                                        theorem update_le_self_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
                                                        Function.update x i a x a x i
                                                        @[simp]
                                                        theorem lt_update_self_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
                                                        x < Function.update x i a x i < a
                                                        @[simp]
                                                        theorem update_lt_self_iff {ι : Type u_1} {π : ιType u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
                                                        Function.update x i a < x a < x i
                                                        instance Pi.sdiff {ι : Type u_1} {π : ιType u_4} [(i : ι) → SDiff (π i)] :
                                                        SDiff ((i : ι) → π i)
                                                        Equations
                                                          theorem Pi.sdiff_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → SDiff (π i)] (x y : (i : ι) → π i) :
                                                          x \ y = fun (i : ι) => x i \ y i
                                                          @[simp]
                                                          theorem Pi.sdiff_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → SDiff (π i)] (x y : (i : ι) → π i) (i : ι) :
                                                          (x \ y) i = x i \ y i
                                                          @[simp]
                                                          theorem Function.const_le_const {α : Type u_2} {β : Type u_3} [Preorder α] [Nonempty β] {a b : α} :
                                                          const β a const β b a b
                                                          @[simp]
                                                          theorem Function.const_lt_const {α : Type u_2} {β : Type u_3} [Preorder α] [Nonempty β] {a b : α} :
                                                          const β a < const β b a < b

                                                          Lifts of order instances #

                                                          @[reducible, inline]
                                                          abbrev Preorder.lift {α : Type u_2} {β : Type u_3} [Preorder β] (f : αβ) :

                                                          Transfer a Preorder on β to a Preorder on α using a function f : α → β. See note [reducible non-instances].

                                                          Equations
                                                            Instances For
                                                              @[reducible, inline]
                                                              abbrev PartialOrder.lift {α : Type u_2} {β : Type u_3} [PartialOrder β] (f : αβ) (inj : Function.Injective f) :

                                                              Transfer a PartialOrder on β to a PartialOrder on α using an injective function f : α → β. See note [reducible non-instances].

                                                              Equations
                                                                Instances For
                                                                  theorem compare_of_injective_eq_compareOfLessAndEq {α : Type u_2} {β : Type u_3} (a b : α) [LinearOrder β] [DecidableEq α] (f : αβ) (inj : Function.Injective f) [Decidable (a < b)] :
                                                                  compare (f a) (f b) = compareOfLessAndEq a b
                                                                  @[reducible, inline]
                                                                  abbrev LinearOrder.lift {α : Type u_2} {β : Type u_3} [LinearOrder β] [Max α] [Min α] (f : αβ) (inj : Function.Injective f) (hsup : ∀ (x y : α), f (xy) = max (f x) (f y)) (hinf : ∀ (x y : α), f (xy) = min (f x) (f y)) :

                                                                  Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Max α] and [Min α] as arguments, then uses them for max and min fields. See LinearOrder.lift' for a version that autogenerates min and max fields, and LinearOrder.liftWithOrd for one that does not auto-generate compare fields. See note [reducible non-instances].

                                                                  Equations
                                                                    Instances For
                                                                      @[reducible, inline]
                                                                      abbrev LinearOrder.lift' {α : Type u_2} {β : Type u_3} [LinearOrder β] (f : αβ) (inj : Function.Injective f) :

                                                                      Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version autogenerates min and max fields. See LinearOrder.lift for a version that takes [Max α] and [Min α], then uses them as max and min. See LinearOrder.liftWithOrd' for a version which does not auto-generate compare fields. See note [reducible non-instances].

                                                                      Equations
                                                                        Instances For
                                                                          @[reducible, inline]
                                                                          abbrev LinearOrder.liftWithOrd {α : Type u_2} {β : Type u_3} [LinearOrder β] [Max α] [Min α] [Ord α] (f : αβ) (inj : Function.Injective f) (hsup : ∀ (x y : α), f (xy) = max (f x) (f y)) (hinf : ∀ (x y : α), f (xy) = min (f x) (f y)) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) :

                                                                          Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Max α] and [Min α] as arguments, then uses them for max and min fields. It also takes [Ord α] as an argument and uses them for compare fields. See LinearOrder.lift for a version that autogenerates compare fields, and LinearOrder.liftWithOrd' for one that auto-generates min and max fields. fields. See note [reducible non-instances].

                                                                          Equations
                                                                            Instances For
                                                                              @[reducible, inline]
                                                                              abbrev LinearOrder.liftWithOrd' {α : Type u_2} {β : Type u_3} [LinearOrder β] [Ord α] (f : αβ) (inj : Function.Injective f) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) :

                                                                              Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version auto-generates min and max fields. It also takes [Ord α] as an argument and uses them for compare fields. See LinearOrder.lift for a version that autogenerates compare fields, and LinearOrder.liftWithOrd for one that doesn't auto-generate min and max fields. fields. See note [reducible non-instances].

                                                                              Equations
                                                                                Instances For

                                                                                  Subtype of an order #

                                                                                  instance Subtype.le {α : Type u_2} [LE α] {p : αProp} :
                                                                                  Equations
                                                                                    instance Subtype.lt {α : Type u_2} [LT α] {p : αProp} :
                                                                                    Equations
                                                                                      @[simp]
                                                                                      theorem Subtype.mk_le_mk {α : Type u_2} [LE α] {p : αProp} {x y : α} {hx : p x} {hy : p y} :
                                                                                      x, hx y, hy x y
                                                                                      @[simp]
                                                                                      theorem Subtype.mk_lt_mk {α : Type u_2} [LT α] {p : αProp} {x y : α} {hx : p x} {hy : p y} :
                                                                                      x, hx < y, hy x < y
                                                                                      @[simp]
                                                                                      theorem Subtype.coe_le_coe {α : Type u_2} [LE α] {p : αProp} {x y : Subtype p} :
                                                                                      x y x y
                                                                                      theorem Subtype.GCongr.coe_le_coe {α : Type u_2} [LE α] {p : αProp} {x y : Subtype p} :
                                                                                      x yx y

                                                                                      Alias of the reverse direction of Subtype.coe_le_coe.

                                                                                      @[simp]
                                                                                      theorem Subtype.coe_lt_coe {α : Type u_2} [LT α] {p : αProp} {x y : Subtype p} :
                                                                                      x < y x < y
                                                                                      theorem Subtype.GCongr.coe_lt_coe {α : Type u_2} [LT α] {p : αProp} {x y : Subtype p} :
                                                                                      x < yx < y

                                                                                      Alias of the reverse direction of Subtype.coe_lt_coe.

                                                                                      instance Subtype.preorder {α : Type u_2} [Preorder α] (p : αProp) :
                                                                                      Equations
                                                                                        instance Subtype.partialOrder {α : Type u_2} [PartialOrder α] (p : αProp) :
                                                                                        Equations
                                                                                          instance Subtype.decidableLE {α : Type u_2} [Preorder α] [h : DecidableLE α] {p : αProp} :
                                                                                          Equations
                                                                                            instance Subtype.decidableLT {α : Type u_2} [Preorder α] [h : DecidableLT α] {p : αProp} :
                                                                                            Equations
                                                                                              instance Subtype.instLinearOrder {α : Type u_2} [LinearOrder α] (p : αProp) :

                                                                                              A subtype of a linear order is a linear order. We explicitly give the proofs of decidable equality and decidable order in order to ensure the decidability instances are all definitionally equal.

                                                                                              Equations

                                                                                                Pointwise order on α × β #

                                                                                                The lexicographic order is defined in Data.Prod.Lex, and the instances are available via the type synonym α ×ₗ β = α × β.

                                                                                                instance Prod.instLE_mathlib {α : Type u_2} {β : Type u_3} [LE α] [LE β] :
                                                                                                LE (α × β)
                                                                                                Equations
                                                                                                  instance Prod.instDecidableLE {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x y : α × β} [Decidable (x.fst y.fst)] [Decidable (x.snd y.snd)] :
                                                                                                  Equations
                                                                                                    theorem Prod.le_def {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x y : α × β} :
                                                                                                    x y x.fst y.fst x.snd y.snd
                                                                                                    @[simp]
                                                                                                    theorem Prod.mk_le_mk {α : Type u_2} {β : Type u_3} [LE α] [LE β] {a₁ a₂ : α} {b₁ b₂ : β} :
                                                                                                    (a₁, b₁) (a₂, b₂) a₁ a₂ b₁ b₂
                                                                                                    theorem Prod.GCongr.mk_le_mk {α : Type u_2} {β : Type u_3} [LE α] [LE β] {a₁ a₂ : α} {b₁ b₂ : β} (ha : a₁ a₂) (hb : b₁ b₂) :
                                                                                                    (a₁, b₁) (a₂, b₂)
                                                                                                    @[simp]
                                                                                                    theorem Prod.swap_le_swap {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x y : α × β} :
                                                                                                    x.swap y.swap x y
                                                                                                    @[simp]
                                                                                                    theorem Prod.swap_le_mk {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x : α × β} {a : α} {b : β} :
                                                                                                    x.swap (b, a) x (a, b)
                                                                                                    @[simp]
                                                                                                    theorem Prod.mk_le_swap {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x : α × β} {a : α} {b : β} :
                                                                                                    (b, a) x.swap (a, b) x
                                                                                                    instance Prod.instPreorder {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] :
                                                                                                    Preorder (α × β)
                                                                                                    Equations
                                                                                                      @[simp]
                                                                                                      theorem Prod.swap_lt_swap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {x y : α × β} :
                                                                                                      x.swap < y.swap x < y
                                                                                                      @[simp]
                                                                                                      theorem Prod.swap_lt_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a : α} {b : β} {x : α × β} :
                                                                                                      x.swap < (b, a) x < (a, b)
                                                                                                      @[simp]
                                                                                                      theorem Prod.mk_lt_swap {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a : α} {b : β} {x : α × β} :
                                                                                                      (b, a) < x.swap (a, b) < x
                                                                                                      theorem Prod.mk_le_mk_iff_left {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b : β} :
                                                                                                      (a₁, b) (a₂, b) a₁ a₂
                                                                                                      theorem Prod.mk_le_mk_iff_right {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a : α} {b₁ b₂ : β} :
                                                                                                      (a, b₁) (a, b₂) b₁ b₂
                                                                                                      theorem Prod.GCongr.mk_le_mk_left {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b : β} :
                                                                                                      a₁ a₂(a₁, b) (a₂, b)

                                                                                                      Alias of the reverse direction of Prod.mk_le_mk_iff_left.

                                                                                                      theorem Prod.GCongr.mk_le_mk_right {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a : α} {b₁ b₂ : β} :
                                                                                                      b₁ b₂(a, b₁) (a, b₂)

                                                                                                      Alias of the reverse direction of Prod.mk_le_mk_iff_right.

                                                                                                      theorem Prod.mk_lt_mk_iff_left {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b : β} :
                                                                                                      (a₁, b) < (a₂, b) a₁ < a₂
                                                                                                      theorem Prod.mk_lt_mk_iff_right {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a : α} {b₁ b₂ : β} :
                                                                                                      (a, b₁) < (a, b₂) b₁ < b₂
                                                                                                      theorem Prod.lt_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {x y : α × β} :
                                                                                                      x < y x.fst < y.fst x.snd y.snd x.fst y.fst x.snd < y.snd
                                                                                                      @[simp]
                                                                                                      theorem Prod.mk_lt_mk {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b₁ b₂ : β} :
                                                                                                      (a₁, b₁) < (a₂, b₂) a₁ < a₂ b₁ b₂ a₁ a₂ b₁ < b₂
                                                                                                      theorem Prod.lt_of_lt_of_le {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {x y : α × β} (h₁ : x.fst < y.fst) (h₂ : x.snd y.snd) :
                                                                                                      x < y
                                                                                                      theorem Prod.lt_of_le_of_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {x y : α × β} (h₁ : x.fst y.fst) (h₂ : x.snd < y.snd) :
                                                                                                      x < y
                                                                                                      theorem Prod.mk_lt_mk_of_lt_of_le {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b₁ b₂ : β} (h₁ : a₁ < a₂) (h₂ : b₁ b₂) :
                                                                                                      (a₁, b₁) < (a₂, b₂)
                                                                                                      theorem Prod.mk_lt_mk_of_le_of_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {a₁ a₂ : α} {b₁ b₂ : β} (h₁ : a₁ a₂) (h₂ : b₁ < b₂) :
                                                                                                      (a₁, b₁) < (a₂, b₂)
                                                                                                      instance Prod.instPartialOrder (α : Type u_5) (β : Type u_6) [PartialOrder α] [PartialOrder β] :

                                                                                                      The pointwise partial order on a product. (The lexicographic ordering is defined in Order.Lexicographic, and the instances are available via the type synonym α ×ₗ β = α × β.)

                                                                                                      Equations

                                                                                                        Additional order classes #

                                                                                                        class DenselyOrdered (α : Type u_5) [LT α] :

                                                                                                        An order is dense if there is an element between any pair of distinct comparable elements.

                                                                                                        • dense (a₁ a₂ : α) : a₁ < a₂ (a : α), a₁ < a a < a₂

                                                                                                          An order is dense if there is an element between any pair of distinct elements.

                                                                                                        Instances
                                                                                                          theorem exists_between {α : Type u_2} [LT α] [DenselyOrdered α] {a₁ a₂ : α} :
                                                                                                          a₁ < a₂ (a : α), a₁ < a a < a₂

                                                                                                          Any ordered subsingleton is densely ordered. Not an instance to avoid a heavy subsingleton typeclass search.

                                                                                                          instance instDenselyOrderedProd {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
                                                                                                          instance instDenselyOrderedForall {ι : Type u_1} {π : ιType u_4} [(i : ι) → Preorder (π i)] [∀ (i : ι), DenselyOrdered (π i)] :
                                                                                                          DenselyOrdered ((i : ι) → π i)
                                                                                                          theorem le_of_forall_gt_imp_ge_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < aa₁ a) :
                                                                                                          a₁ a₂
                                                                                                          theorem forall_gt_imp_ge_iff_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} :
                                                                                                          (∀ (a : α), a₂ < aa₁ a) a₁ a₂
                                                                                                          theorem eq_of_le_of_forall_lt_imp_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a₂ < aa₁ a) :
                                                                                                          a₁ = a₂
                                                                                                          theorem le_of_forall_lt_imp_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h : ∀ (a : α), a < a₁a a₂) :
                                                                                                          a₁ a₂
                                                                                                          theorem forall_lt_imp_le_iff_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} :
                                                                                                          (∀ (a : α), a < a₁a a₂) a₁ a₂
                                                                                                          theorem eq_of_le_of_forall_gt_imp_ge_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a < a₁a a₂) :
                                                                                                          a₁ = a₂
                                                                                                          @[deprecated le_of_forall_gt_imp_ge_of_dense (since := "2025-01-21")]
                                                                                                          theorem le_of_forall_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h : ∀ (a : α), a₂ < aa₁ a) :
                                                                                                          a₁ a₂

                                                                                                          Alias of le_of_forall_gt_imp_ge_of_dense.

                                                                                                          @[deprecated le_of_forall_lt_imp_le_of_dense (since := "2025-01-21")]
                                                                                                          theorem le_of_forall_ge_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h : ∀ (a : α), a < a₁a a₂) :
                                                                                                          a₁ a₂

                                                                                                          Alias of le_of_forall_lt_imp_le_of_dense.

                                                                                                          @[deprecated forall_lt_imp_le_iff_le_of_dense (since := "2025-01-21")]
                                                                                                          theorem forall_lt_le_iff {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} :
                                                                                                          (∀ (a : α), a < a₁a a₂) a₁ a₂

                                                                                                          Alias of forall_lt_imp_le_iff_le_of_dense.

                                                                                                          @[deprecated forall_gt_imp_ge_iff_le_of_dense (since := "2025-01-21")]
                                                                                                          theorem forall_gt_ge_iff {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} :
                                                                                                          (∀ (a : α), a₂ < aa₁ a) a₁ a₂

                                                                                                          Alias of forall_gt_imp_ge_iff_le_of_dense.

                                                                                                          @[deprecated eq_of_le_of_forall_lt_imp_le_of_dense (since := "2025-01-21")]
                                                                                                          theorem eq_of_le_of_forall_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a₂ < aa₁ a) :
                                                                                                          a₁ = a₂

                                                                                                          Alias of eq_of_le_of_forall_lt_imp_le_of_dense.

                                                                                                          @[deprecated eq_of_le_of_forall_gt_imp_ge_of_dense (since := "2025-01-21")]
                                                                                                          theorem eq_of_le_of_forall_ge_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a < a₁a a₂) :
                                                                                                          a₁ = a₂

                                                                                                          Alias of eq_of_le_of_forall_gt_imp_ge_of_dense.

                                                                                                          theorem dense_or_discrete {α : Type u_2} [LinearOrder α] (a₁ a₂ : α) :
                                                                                                          ( (a : α), a₁ < a a < a₂) (∀ (a : α), a₁ < aa₂ a) ∀ (a : α), a < a₂a a₁
                                                                                                          theorem eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type u_2} [LinearOrder α] (h : ∀ ⦃x y z : α⦄, x < yy < zFalse) (x y z : α) :
                                                                                                          x = y y = z x = z

                                                                                                          If a linear order has no elements x < y < z, then it has at most two elements.

                                                                                                          theorem PUnit.le (a b : PUnit.{u_5 + 1}) :
                                                                                                          a b
                                                                                                          instance Prop.le :

                                                                                                          Propositions form a complete boolean algebra, where the relation is given by implication.

                                                                                                          Equations
                                                                                                            @[simp]
                                                                                                            theorem le_Prop_eq :
                                                                                                            (fun (x1 x2 : Prop) => x1 x2) = fun (x1 x2 : Prop) => x1x2
                                                                                                            theorem subrelation_iff_le {α : Type u_2} {r s : ααProp} :

                                                                                                            Linear order from a total partial order #

                                                                                                            def AsLinearOrder (α : Type u_5) :
                                                                                                            Type u_5

                                                                                                            Type synonym to create an instance of LinearOrder from a PartialOrder and IsTotal α (≤)

                                                                                                            Equations
                                                                                                              Instances For
                                                                                                                noncomputable instance AsLinearOrder.linearOrder {α : Type u_2} [PartialOrder α] [IsTotal α fun (x1 x2 : α) => x1 x2] :
                                                                                                                Equations