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.

Transferring orders

• Order.Preimage, Preorder.lift: Transfers a (pre)order on β to an order on α using a function f : α → β.
• PartialOrder.lift, LinearOrder.lift: Transfers a partial (resp., linear) order on β to a partial (resp., linear) order on α using an injective function f.

Extra class

• DenselyOrdered: An order with no gap, i.e. for any two elements a < b there exists c such that a < c < b.

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

• expand module docs

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 α] {a b : α} (h : a ≤ b) : b ≥ a

theorem GE.ge.le {α : Type u_2} [LE α] {a b : α} (h : a ≥ b) : b ≤ a

@[deprecated le_of_eq_of_le (since := "2025-11-29")]

theorem le_of_le_of_eq' {α : Type u_2} [LE α] {a b c : α} : b ≤ c → a = b → a ≤ c

@[deprecated le_of_le_of_eq (since := "2025-11-29")]

theorem le_of_eq_of_le' {α : Type u_2} [LE α] {a b c : α} : b = c → a ≤ b → a ≤ c

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_1} {a b c : α} [LE α] (h₁ : b ≤ a) (h₂ : b = c) : c ≤ a

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_1} {a b c : α} [LE α] (h₁ : a = b) (h₂ : c ≤ b) : c ≤ a

theorem LT.lt.gt {α : Type u_2} [LT α] {a b : α} (h : a < b) : b > a

theorem GT.gt.lt {α : Type u_2} [LT α] {a b : α} (h : a > b) : b < a

@[deprecated lt_of_eq_of_lt (since := "2025-11-29")]

theorem lt_of_lt_of_eq' {α : Type u_2} [LT α] {a b c : α} : b < c → a = b → a < c

@[deprecated lt_of_lt_of_eq (since := "2025-11-29")]

theorem lt_of_eq_of_lt' {α : Type u_2} [LT α] {a b c : α} : b = c → a < b → a < c

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_1} {a b c : α} [LT α] (h₁ : b < a) (h₂ : b = c) : c < a

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_1} {a b c : α} [LT α] (h₁ : a = b) (h₂ : c < b) : c < a

def Order.Preimage {α : Type u_2} {β : Type u_3} (f : α → β) (s : β → β → Prop) (x y : α) : Prop

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).

def «term_⁻¹'o_» : Lean.TrailingParserDescr

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).

instance Order.Preimage.decidable {α : Type u_2} {β : Type u_3} (f : α → β) (s : β → β → Prop) [H : DecidableRel s] : DecidableRel (f ⁻¹'o s)

The preimage of a decidable order is decidable.

Preorders

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_ge {α : Type u_2} [Preorder α] {a b : α} : ¬a < b ↔ a ≤ b → b ≤ a

@[simp]

theorem lt_self_iff_false {α : Type u_2} [Preorder α] (x : α) : x < x ↔ False

theorem le_trans' {α : Type u_1} [Preorder α] {a b c : α} : b ≤ a → c ≤ b → c ≤ a

Alias of ge_trans.

theorem ge_trans' {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

theorem lt_trans' {α : Type u_1} [Preorder α] {a b c : α} : b < a → c < b → c < a

Alias of gt_trans.

theorem gt_trans' {α : Type u_1} [Preorder α] {a b c : α} : a < b → b < c → a < c

theorem LE.le.trans {α : Type u_1} [Preorder α] {a b c : α} : a ≤ b → b ≤ c → a ≤ c

Alias of le_trans.

theorem LE.le.trans' {α : Type u_1} [Preorder α] {a b c : α} : b ≤ a → c ≤ b → c ≤ a

theorem LT.lt.trans {α : Type u_1} [Preorder α] {a b c : α} : a < b → b < c → a < c

Alias of lt_trans.

theorem LT.lt.trans' {α : Type u_1} [Preorder α] {a b c : α} : b < a → c < b → c < a

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_1} [Preorder α] {a b c : α} (hab : b ≤ a) (hbc : c < b) : c < a

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_1} [Preorder α] {a b c : α} (hab : b < a) (hbc : c ≤ b) : c < a

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

Alias of lt_of_le_not_ge.

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

Alias of le_of_lt.

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

Alias of lt_asymm.

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

Alias of lt_asymm.

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

Alias of ne_of_lt.

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

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

Alias of le_of_eq.

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

theorem LT.lt.false {α : Type u_2} [Preorder α] {a : α} : a < a → False

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

theorem ne_of_not_le {α : Type u_2} [Preorder α] {a b : α} (h : ¬a ≤ b) : a ≠ b

theorem ne_of_not_ge {α : Type u_2} [Preorder α] {a b : α} (h : ¬b ≤ a) : a ≠ b

@[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 le_of_forall_le {α : Type u_2} [Preorder α] {a b : α} (H : ∀ c ≤ a, c ≤ b) : a ≤ b

theorem le_of_forall_ge {α : Type u_2} [Preorder α] {a b : α} (H : ∀ (c : α), a ≤ c → b ≤ c) : b ≤ a

theorem forall_le_iff_le {α : Type u_2} [Preorder α] {a b : α} : (∀ ⦃c : α⦄, c ≤ a → c ≤ b) ↔ a ≤ b

theorem forall_ge_iff_le {α : Type u_2} [Preorder α] {a b : α} : (∀ ⦃c : α⦄, a ≤ c → b ≤ c) ↔ b ≤ a

theorem le_imp_le_of_le_of_le {α : Type u_2} [Preorder α] {a b c d : α} (h₁ : c ≤ a) (h₂ : b ≤ d) : a ≤ b → c ≤ d

monotonicity of ≤ with respect to →

theorem lt_imp_lt_of_le_of_le {α : Type u_2} [Preorder α] {a b c d : α} (h₁ : c ≤ a) (h₂ : b ≤ d) : a < b → c < d

monotonicity of < with respect to →

def Mathlib.Tactic.GCongr.exactLeOfLt : ForwardExt

See if the term is a < b and the goal is a ≤ b.

Partial order

theorem Ne.lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} : a ≠ b → a ≤ b → a < b

theorem Ne.lt_of_le' {α : Type u_2} [PartialOrder α] {a b : α} : a ≠ b → b ≤ a → b < a

theorem LE.le.antisymm {α : Type u_1} [PartialOrder α] {a b : α} : a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem LE.le.antisymm' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → a ≤ b → a = b

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

Alias of lt_of_le_of_ne.

theorem LE.le.lt_of_ne' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → a ≠ b → b < a

theorem LE.le.lt_iff_ne {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) : a < b ↔ a ≠ b

theorem LE.le.lt_iff_ne' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) : b < a ↔ a ≠ b

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

theorem LE.le.not_lt_iff_eq' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) : ¬b < a ↔ a = b

theorem LE.le.ge_iff_eq {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) : b ≤ a ↔ a = b

theorem LE.le.ge_iff_eq' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) : a ≤ b ↔ a = b

theorem le_imp_eq_iff_le_imp_ge {α : Type u_2} [PartialOrder α] {a b : α} : a ≤ b → a = b ↔ a ≤ b → b ≤ a

theorem le_imp_eq_iff_le_imp_ge' {α : Type u_2} [PartialOrder α] {a b : α} : b ≤ a → 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 Decidable.le_iff_eq_or_lt' {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] : b ≤ a ↔ a = b ∨ b < a

theorem le_iff_eq_or_lt {α : Type u_2} [PartialOrder α] {a b : α} : a ≤ b ↔ a = b ∨ a < b

theorem le_iff_eq_or_lt' {α : Type u_2} [PartialOrder α] {a b : α} : b ≤ a ↔ a = b ∨ b < a

theorem lt_iff_le_and_ne {α : Type u_2} [PartialOrder α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b

theorem lt_iff_le_and_ne' {α : Type u_2} [PartialOrder α] {a b : α} : b < a ↔ b ≤ a ∧ a ≠ b

theorem Decidable.eq_iff_le_not_lt {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] : a = b ↔ a ≤ b ∧ ¬a < b

theorem Decidable.eq_iff_ge_not_gt {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] : a = b ↔ b ≤ a ∧ ¬b < a

theorem eq_iff_le_not_lt {α : Type u_2} [PartialOrder α] {a b : α} : a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_iff_ge_not_gt {α : Type u_2} [PartialOrder α] {a b : α} : a = b ↔ b ≤ a ∧ ¬b < a

theorem Decidable.eq_or_lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] (h : a ≤ b) : a = b ∨ a < b

theorem Decidable.eq_or_lt_of_le' {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] (h : b ≤ a) : a = b ∨ b < a

theorem eq_or_lt_of_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≤ b) : a = b ∨ a < b

theorem eq_or_lt_of_le' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) : a = b ∨ b < a

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 LE.le.lt_or_eq_dec' {α : Type u_1} [PartialOrder α] {a b : α} [DecidableLE α] (hab : b ≤ a) : b < a ∨ a = b

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

Alias of Decidable.eq_or_lt_of_le.

theorem LE.le.eq_or_lt_dec' {α : Type u_2} [PartialOrder α] {a b : α} [DecidableLE α] (h : b ≤ a) : a = b ∨ b < a

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

Alias of lt_or_eq_of_le.

theorem LE.le.lt_or_eq' {α : Type u_1} [PartialOrder α] {a b : α} : b ≤ a → b < a ∨ a = b

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_lt' {α : Type u_2} [PartialOrder α] {a b : α} (h : b ≤ a) : a = b ∨ b < a

theorem eq_of_le_of_not_lt {α : Type u_2} [PartialOrder α] {a b : α} (h₁ : a ≤ b) (h₂ : ¬a < b) : a = b

theorem eq_of_le_of_not_lt' {α : Type u_2} [PartialOrder α] {a b : α} (h₁ : b ≤ a) (h₂ : ¬b < a) : a = b

theorem LE.le.eq_of_not_lt {α : Type u_2} [PartialOrder α] {a b : α} (h₁ : a ≤ b) (h₂ : ¬a < b) : a = b

Alias of eq_of_le_of_not_lt.

theorem LE.le.eq_of_not_lt' {α : Type u_2} [PartialOrder α] {a b : α} (h₁ : b ≤ a) (h₂ : ¬b < a) : a = b

theorem Ne.le_iff_lt {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a < b

theorem Ne.ge_iff_gt {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≠ b) : b ≤ a ↔ b < a

theorem Ne.not_le_or_not_ge {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≠ b) : ¬a ≤ b ∨ ¬b ≤ a

theorem Ne.not_ge_or_not_le {α : Type u_2} [PartialOrder α] {a b : α} (h : a ≠ b) : ¬b ≤ a ∨ ¬a ≤ b

theorem Decidable.ne_iff_lt_iff_le {α : Type u_2} [PartialOrder α] {a b : α} [DecidableEq α] : (a ≠ b ↔ a < b) ↔ a ≤ b

theorem Decidable.ne_iff_gt_iff_ge {α : Type u_2} [PartialOrder α] {a b : α} [DecidableEq α] : (a ≠ b ↔ b < a) ↔ b ≤ a

@[simp]

theorem ne_iff_lt_iff_le {α : Type u_2} [PartialOrder α] {a b : α} : (a ≠ b ↔ a < b) ↔ a ≤ b

@[simp]

theorem ne_iff_gt_iff_ge {α : Type u_2} [PartialOrder α] {a b : α} : (a ≠ b ↔ b < a) ↔ b ≤ a

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)) : Std.Associative f

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.gt_or_le {α : Type u_2} [LinearOrder α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b

theorem LE.le.lt_or_ge {α : Type u_2} [LinearOrder α] {a b : α} (h : b ≤ a) (c : α) : c < a ∨ b ≤ c

theorem LE.le.ge_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c < b

theorem LE.le.le_or_gt {α : Type u_2} [LinearOrder α] {a b : α} (h : b ≤ a) (c : α) : c ≤ a ∨ b < c

theorem LE.le.ge_or_le {α : Type u_2} [LinearOrder α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c ≤ b

theorem LE.le.le_or_ge {α : Type u_2} [LinearOrder α] {a b : α} (h : b ≤ a) (c : α) : c ≤ a ∨ b ≤ c

theorem LT.lt.gt_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a < b) (c : α) : a < c ∨ c < b

theorem LT.lt.lt_or_gt {α : Type u_2} [LinearOrder α] {a b : α} (h : b < a) (c : α) : c < a ∨ b < c

theorem Ne.lt_or_gt {α : Type u_2} [LinearOrder α] {a b : α} (h : a ≠ b) : a < b ∨ b < a

theorem Ne.gt_or_lt {α : Type u_2} [LinearOrder α] {a b : α} (h : a ≠ b) : b < a ∨ a < b

@[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 lt_or_gt_iff_ne' {α : Type u_2} [LinearOrder α] {a b : α} : b < a ∨ a < b ↔ a ≠ b

theorem not_lt_iff_eq_or_lt {α : Type u_2} [LinearOrder α] {a b : α} : ¬a < b ↔ a = b ∨ b < a

theorem not_lt_iff_eq_or_lt' {α : Type u_2} [LinearOrder α] {a b : α} : ¬b < a ↔ a = b ∨ a < b

theorem exists_ge_of_linear {α : Type u_2} [LinearOrder α] (a b : α) : ∃ (c : α), a ≤ c ∧ b ≤ c

theorem exists_le_of_linear {α : Type u_2} [LinearOrder α] (a b : α) : ∃ c ≤ a, c ≤ b

theorem exists_forall_ge_and {α : Type u_2} [LinearOrder α] {p q : α → Prop} : (∃ (i : α), ∀ j ≥ i, p j) → (∃ (i : α), ∀ j ≥ i, q j) → ∃ (i : α), ∀ j ≥ i, p j ∧ q j

theorem exists_forall_le_and {α : Type u_2} [LinearOrder α] {p q : α → Prop} : (∃ (i : α), ∀ (j : α), i ≥ j → p j) → (∃ (i : α), ∀ (j : α), i ≥ j → q j) → ∃ (i : α), ∀ (j : α), i ≥ j → p j ∧ q j

theorem le_of_forall_lt {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ c < a, c < b) : a ≤ b

theorem le_of_forall_gt {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), a < c → b < c) : b ≤ a

theorem forall_lt_iff_le {α : Type u_2} [LinearOrder α] {a b : α} : (∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b

theorem forall_gt_iff_le {α : Type u_2} [LinearOrder α] {a b : α} : (∀ ⦃c : α⦄, a < c → b < c) ↔ b ≤ a

theorem le_of_forall_lt_imp_ne {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ c < a, c ≠ b) : a ≤ b

theorem le_of_forall_gt_imp_ne {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), a < c → c ≠ b) : b ≤ a

theorem lt_of_forall_le_imp_ne {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ c ≤ a, c ≠ b) : a < b

theorem lt_of_forall_ge_imp_ne {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), a ≤ c → c ≠ b) : b < a

theorem forall_lt_imp_ne_iff_le {α : Type u_2} [LinearOrder α] {a b : α} : (∀ c < a, c ≠ b) ↔ a ≤ b

theorem forall_gt_imp_ne_iff_le {α : Type u_2} [LinearOrder α] {a b : α} : (∀ (c : α), a < c → c ≠ b) ↔ b ≤ a

theorem forall_le_imp_ne_iff_lt {α : Type u_2} [LinearOrder α] {a b : α} : (∀ c ≤ a, c ≠ b) ↔ a < b

theorem forall_ge_imp_ne_iff_lt {α : Type u_2} [LinearOrder α] {a b : α} : (∀ (c : α), a ≤ c → c ≠ b) ↔ 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

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'

min/max recursors

theorem min_rec {α : Type u_2} [LinearOrder α] {a b : α} {p : α → Prop} (ha : a ≤ b → p a) (hb : b ≤ a → p b) : p (min a b)

theorem max_rec {α : Type u_2} [LinearOrder α] {a b : α} {p : α → Prop} (ha : b ≤ a → p a) (hb : a ≤ b → p 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 b < a then a else b

theorem max_def_lt {α : Type u_2} [LinearOrder α] (a b : α) : max a b = if a < b then b else a

theorem min_def_lt' {α : Type u_2} [LinearOrder α] (a b : α) : min a b = if b < a 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 ≤ b → c ≤ 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 ≤ b → c ≤ d ↔ d < c → b < 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) [Std.Symm r] {f : α → β} (h : ∀ (a b : α), r a b → f a ≤ f b) {a b : α} : r a b → f a = f b

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

Extensionality lemmas

theorem Preorder.toLE_injective {α : Type u_2} : Function.Injective (@toLE α)

theorem Preorder.toLE_injective_iff {α : Type u_2} {a₁ a₂ : Preorder α} : a₁ = a₂ ↔ a₁.toLE = a₂.toLE

theorem PartialOrder.toPreorder_injective {α : Type u_2} : Function.Injective (@toPreorder α)

theorem PartialOrder.toPreorder_injective_iff {α : Type u_2} {a₁ a₂ : PartialOrder α} : a₁ = a₂ ↔ a₁.toPreorder = a₂.toPreorder

theorem LinearOrder.toPartialOrder_injective {α : Type u_2} : Function.Injective (@toPartialOrder α)

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

Compl

instance Prop.instCompl : Compl Prop

instance Pi.instCompl {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → Compl (π i)] : Compl ((i : ι) → π i)

theorem Pi.compl_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → Compl (π i)] (x : (i : ι) → π i) : xᶜ = fun (i : ι) => (x i)ᶜ

@[simp]

theorem Pi.compl_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → Compl (π i)] (x : (i : ι) → π i) (i : ι) : xᶜ i = (x i)ᶜ

instance Std.Irrefl.compl {α : Type u_2} (r : α → α → Prop) [Irrefl r] : Refl rᶜ

instance Std.Refl.compl {α : Type u_2} (r : α → α → Prop) [Refl r] : Irrefl 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)

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)

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)

@[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) : Prop

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

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) : StrongLT a c

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

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) : StrongLT a 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} (hbc : c ≤ b) (hab : StrongLT b a) : StrongLT c a

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 ≠ i → x 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 y i a ≤ x ↔ a ≤ x i ∧ ∀ (j : ι), j ≠ i → y j ≤ x 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 ≠ i → x 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} : Function.update x i a ≤ Function.update x i b ↔ a ≤ b

@[simp]

theorem update_lt_update_iff {ι : Type u_1} {π : ι → Type u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a b : π i} : Function.update x i a < Function.update x i b ↔ a < b

@[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)

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

Pullbacks of order instances

@[reducible, inline]

abbrev Function.Injective.preorder {α : Type u_2} {β : Type u_3} [Preorder β] [LE α] [LT α] (f : α → β) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) : Preorder α

Pull back a Preorder instance along an injective function.

See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.partialOrder {α : Type u_2} {β : Type u_3} [PartialOrder β] [LE α] [LT α] (f : α → β) (hf : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) : PartialOrder α

Pull back a PartialOrder instance along an injective function.

See note [reducible non-instances].

@[reducible, inline]

abbrev Function.Injective.linearOrder {α : Type u_2} {β : Type u_3} [LinearOrder β] [LE α] [LT α] [Max α] [Min α] [Ord α] [DecidableEq α] [DecidableLE α] [DecidableLT α] (f : α → β) (hf : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (min : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) (max : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) (compare : ∀ (x y : α), compare (f x) (f y) = compare x y) : LinearOrder α

Pull back a LinearOrder instance along an injective function.

See note [reducible non-instances].

Lifts of order instances

Unlike the constructions above, these construct new data fields. They should be avoided if the types already define any order or decidability instances.

@[reducible, inline]

abbrev Preorder.lift {α : Type u_2} {β : Type u_3} [Preorder β] (f : α → β) : Preorder α

Transfer a Preorder on β to a Preorder on α using a function f : α → β.

See also Function.Injective.preorder when only the proof fields need to be transferred.

See note [reducible non-instances].

@[reducible, inline]

abbrev PartialOrder.lift {α : Type u_2} {β : Type u_3} [PartialOrder β] (f : α → β) (inj : Function.Injective f) : PartialOrder α

Transfer a PartialOrder on β to a PartialOrder on α using an injective function f : α → β.

See also Function.Injective.partialOrder when only the proof fields need to be transferred.

See note [reducible non-instances].

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 (x ⊔ y) = max (f x) (f y)) (hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) : LinearOrder α

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 also Function.Injective.linearOrder when only the proof fields need to be transferred.

See note [reducible non-instances].

@[reducible, inline]

abbrev LinearOrder.lift' {α : Type u_2} {β : Type u_3} [LinearOrder β] (f : α → β) (inj : Function.Injective f) : LinearOrder α

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].

@[reducible, inline]

abbrev LinearOrder.liftWithOrd {α : Type u_2} {β : Type u_3} [LinearOrder β] [Max α] [Min α] [Ord α] (f : α → β) (inj : Function.Injective f) (hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y)) (hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) : LinearOrder α

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].

@[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)) : LinearOrder α

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].

Subtype of an order

@[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

@[simp]

theorem Subtype.coe_lt_coe {α : Type u_2} [LT α] {p : α → Prop} {x y : Subtype p} : ↑x < ↑y ↔ x < y

instance Subtype.preorder {α : Type u_2} [Preorder α] (p : α → Prop) : Preorder (Subtype p)

instance Subtype.partialOrder {α : Type u_2} [PartialOrder α] (p : α → Prop) : PartialOrder (Subtype p)

instance Subtype.decidableLE {α : Type u_2} [Preorder α] [h : DecidableLE α] {p : α → Prop} : DecidableLE (Subtype p)

instance Subtype.decidableLT {α : Type u_2} [Preorder α] [h : DecidableLT α] {p : α → Prop} : DecidableLT (Subtype p)

instance Subtype.instLinearOrder {α : Type u_2} [LinearOrder α] (p : α → Prop) : LinearOrder (Subtype p)

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.

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 (α × β)

instance Prod.instDecidableLE {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x y : α × β} [Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] : Decidable (x ≤ y)

theorem Prod.le_def {α : Type u_2} {β : Type u_3} [LE α] [LE β] {x y : α × β} : x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2

@[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 (α × β)

@[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.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.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2

@[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.1 < y.1) (h₂ : x.2 ≤ y.2) : x < y

theorem Prod.lt_of_le_of_lt {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {x y : α × β} (h₁ : x.1 ≤ y.1) (h₂ : x.2 < y.2) : 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 β] : 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 α ×ₗ β = α × β.)

Additional order classes

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

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.

theorem DenselyOrdered.dense' {α : Type u_2} [LT α] [DenselyOrdered α] (a₁ a₂ : α) : a₁ < a₂ → ∃ a < a₂, a₁ < a

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

theorem exists_between' {α : Type u_2} [LT α] [DenselyOrdered α] {a₁ a₂ : α} : a₂ < a₁ → ∃ a < a₁, a₂ < a

theorem Subsingleton.instDenselyOrdered {X : Type u_5} [Subsingleton X] [LT X] : DenselyOrdered X

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 β] : 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₂ < a → a₁ ≤ 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₁

theorem forall_gt_imp_ge_iff_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} : (∀ (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₁

theorem eq_of_le_of_forall_lt_imp_le_of_dense {α : Type u_2} [LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : ∀ (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₂

theorem dense_or_discrete {α : Type u_2} [LinearOrder α] (a₁ a₂ : α) : (∃ (a : α), a₁ < a ∧ a < a₂) ∨ (∀ (a : α), a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁

theorem dense_or_discrete' {α : Type u_2} [LinearOrder α] (a₁ a₂ : α) : (∃ a < a₁, a₂ < a) ∨ (∀ a < a₁, a ≤ 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 < y → y < z → False) (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.

@[reducible, inline]

abbrev LinearOrder.ofSubsingleton {α : Type u_5} [Subsingleton α] : LinearOrder α

Construct the trivial linear order on any type with at most one element.

instance instLinearOrderEmpty : LinearOrder Empty

instance instLinearOrderPEmpty : LinearOrder PEmpty.{u_5 + 1}

instance PUnit.instLinearOrder : LinearOrder PUnit.{u_5 + 1}

theorem PUnit.max_eq (a b : PUnit.{u_5 + 1}) : max a b = unit

theorem PUnit.min_eq (a b : PUnit.{u_5 + 1}) : min a b = unit

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

theorem PUnit.not_lt (a b : PUnit.{u_5 + 1}) : ¬a < b

instance PUnit.instDenselyOrdered : DenselyOrdered PUnit.{u_5 + 1}

instance Prop.le : LE Prop

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

@[simp]

theorem le_Prop_eq : (fun (x1 x2 : Prop) => x1 ≤ x2) = fun (x1 x2 : Prop) => x1 → x2

theorem subrelation_iff_le {α : Type u_2} {r s : α → α → Prop} : Subrelation r s ↔ r ≤ s

instance Prop.partialOrder : PartialOrder Prop

@[deprecated "build a `LinearOrder` instance directly instead" (since := "2025-10-28")]

def AsLinearOrder (α : Type u_5) : Type u_5

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

Do not use this: instead, build a LinearOrder instance directly.

@[deprecated "`AsLinearOrder` is deprecated" (since := "2025-10-28")]

instance instInhabitedAsLinearOrder {α : Type u_2} [Inhabited α] : Inhabited (AsLinearOrder α)

@[deprecated "`AsLinearOrder` is deprecated" (since := "2025-10-28")]

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