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.

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

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

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

Alias of le_of_eq_of_le''.

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

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

Alias of lt_of_lt_of_eq''.

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

Alias of lt_of_eq_of_lt''.

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

Equations

• (f ⁻¹'o s) x y = s (f x) (f y)

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

Equations

• «term_⁻¹'o_» = Lean.ParserDescr.trailingNode `«term_⁻¹'o_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⁻¹'o ") (Lean.ParserDescr.cat `term 81))

@[instance_reducible]

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.

Equations

• Order.Preimage.decidable f s x✝¹ x✝ = H (f x✝¹) (f x✝)

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

Alias of le_trans.

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

Alias of lt_trans.

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

Alias of ge_trans.

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

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

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

Alias of lt_of_lt_of_le'.

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

Alias of ne_of_gt.

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

Alias of ge_of_eq.

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 : α), 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 →

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

monotonicity of ≥ with respect to →

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

monotonicity of > with respect to →

theorem ge_imp_gt_of_lt {α : Type u_2} [Preorder α] {a b c : α} (h : a < b) : a ≥ c → b > c

theorem ge_imp_gt_of_lt' {α : Type u_2} [Preorder α] {a b c : α} (h : b < a) : c ≥ a → c > b

def Mathlib.Tactic.GCongr.exactLeOfLt : ForwardExt

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

Equations

• One or more equations did not get rendered due to their size.

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

Alias of ge_antisymm.

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

Alias of lt_of_le_of_ne'.

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

Alias of Decidable.lt_or_eq_of_le'.

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

Alias of Decidable.eq_or_lt_of_le'.

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

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

Alias of eq_or_lt_of_le'.

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

Alias of eq_of_le_of_not_lt'.

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 : α), c ≤ a ∧ c ≤ b

theorem exists_forall_ge_and {α : Type u_2} [LinearOrder α] {p q : α → Prop} : (∃ (i : α), ∀ (j : α), j ≥ i → p j) → (∃ (i : α), ∀ (j : α), j ≥ i → q j) → ∃ (i : α), ∀ (j : α), 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 : α), 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 : α), 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 : α), 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 : α), 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 : α), 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_reducible]

instance Prop.instCompl : Compl Prop

Equations

• «Prop».instCompl = { compl := Not }

@[instance_reducible]

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

Equations

• Pi.instCompl = { compl := fun (x : (i : ι) → π i) (i : ι) => (x i)ᶜ }

@[instance_reducible]

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

Equations

• Pi.instHNot = { hnot := fun (x : (i : ι) → π i) (i : ι) => ￢x i }

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

theorem Pi.hnot_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HNot (π 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)ᶜ

@[simp]

theorem Pi.hnot_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HNot (π 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_reducible]

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

Equations

• Pi.preorder = { toLE := inferInstance, lt := fun (a b : (i : ι) → π i) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

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

Equations

• Pi.partialOrder = { toPreorder := Pi.preorder, le_antisymm := ⋯ }

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

Equations

• StrongLT a b = ∀ (i : ι), a i < b 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

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 ≠ 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_reducible]

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

Equations

• Pi.instSDiff = { sdiff := fun (x y : (i : ι) → π i) (i : ι) => x i \ y i }

@[instance_reducible]

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

Equations

• Pi.instHImp = { himp := fun (y x : (i : ι) → π i) (i : ι) => y i ⇨ x 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

theorem Pi.himp_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (x y : (i : ι) → π i) : y ⇨ x = fun (i : ι) => y i ⇨ x 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 Pi.himp_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HImp (π i)] (x y : (i : ι) → π i) (i : ι) : (y ⇨ x) i = y i ⇨ x 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].

Equations

• Function.Injective.preorder f le lt = { toLE := inst✝¹, toLT := inst✝, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

Equations

• Function.Injective.partialOrder f hf le lt = { toPreorder := Function.Injective.preorder f ⋯ ⋯, le_antisymm := ⋯ }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Preorder.lift f = Function.Injective.preorder f ⋯ ⋯

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

Equations

• PartialOrder.lift f inj = Function.Injective.partialOrder f inj ⋯ ⋯

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

Equations

• LinearOrder.lift f inj hsup hinf = Function.Injective.linearOrder f inj ⋯ ⋯ hinf hsup ⋯

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

Equations

• LinearOrder.lift' f inj = LinearOrder.lift f inj ⋯ ⋯

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

Equations

• LinearOrder.liftWithOrd f inj hsup hinf compare_f = Function.Injective.linearOrder f inj ⋯ ⋯ hinf hsup ⋯

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

Equations

• LinearOrder.liftWithOrd' f inj compare_f = LinearOrder.liftWithOrd f inj ⋯ ⋯ compare_f

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

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

Equations

• Subtype.preorder p = { toLE := Subtype.instLE, toLT := Subtype.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

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

Equations

• Subtype.partialOrder p = { toPreorder := Subtype.preorder p, le_antisymm := ⋯ }

@[instance_reducible]

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

Equations

• a.decidableLE b = h ↑a ↑b

@[instance_reducible]

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

Equations

• a.decidableLT b = h ↑a ↑b

@[instance_reducible]

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.

Equations

• One or more equations did not get rendered due to their size.

Pointwise order on α × β

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

@[instance_reducible]

instance Prod.instLE_mathlib {α : Type u_2} {β : Type u_3} [LE α] [LE β] : LE (α × β)

Equations

• Prod.instLE_mathlib = { le := fun (p q : α × β) => p.fst ≤ q.fst ∧ p.snd ≤ q.snd }

@[instance_reducible]

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

Equations

• Prod.instDecidableLE = { decide := decide (x.fst ≤ y.fst) && decide (x.snd ≤ y.snd), reflects_decide := ⋯ }

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

instance Prod.instPreorder {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] : Preorder (α × β)

Equations

• Prod.instPreorder = { toLE := inferInstance, lt := fun (a b : α × β) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[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.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_reducible]

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 α ×ₗ β = α × β.)

Equations

• Prod.instPartialOrder α β = { toPreorder := inferInstance, le_antisymm := ⋯ }

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₁ < a

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

DenselyOrdered.mk' is the dual of DenselyOrdered.mk, which we need for to_dual. Please avoid using this directly.

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₂ < 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₂ ≤ 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₂ ≤ 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₁ = 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 ≤ 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₁ ≤ 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.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instLinearOrderEmpty : LinearOrder Empty

Equations

• instLinearOrderEmpty = LinearOrder.ofSubsingleton

@[instance_reducible]

instance instLinearOrderPEmpty : LinearOrder PEmpty.{u_5 + 1}

Equations

• instLinearOrderPEmpty = LinearOrder.ofSubsingleton

@[instance_reducible]

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

Equations

• PUnit.instLinearOrder = LinearOrder.ofSubsingleton

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}

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

@[instance_reducible]

instance Prop.partialOrder : PartialOrder Prop

Equations

• One or more equations did not get rendered due to their size.