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 #

OrderDual α : A type synonym reversing the meaning of all inequalities, with notation αᵒᵈ.
AsLinearOrder α: A type synonym to promote PartialOrder α to LinearOrder α using IsTotal α (≤).

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
automatic construction of dual definitions / theorems

Tags #

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

theorem le_trans' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a ≤ b → a ≤ c

theorem lt_trans' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b < c → a < b → a < c

theorem lt_of_le_of_lt' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a < b → a < c

theorem lt_of_lt_of_le' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b < c → a ≤ b → a < c

theorem ge_antisymm {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≤ a → b = a

theorem lt_of_le_of_ne' {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≠ a → a < b

theorem Ne.lt_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≠ b → a ≤ b → a < b

theorem Ne.lt_of_le' {α : Type u} [PartialOrder α] {a : α} {b : α} :

b ≠ a → a ≤ b → a < b

theorem LE.ext {α : Type u} (x : LE α) (y : LE α) (le : LE.le = LE.le) :

x = y

theorem LE.ext_iff {α : Type u} (x : LE α) (y : LE α) :

x = y ↔ LE.le = LE.le

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

a ≤ b → b ≤ c → a ≤ c

Alias of le_trans.

The relation ≤ on a preorder is transitive.

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

b ≤ c → a ≤ b → a ≤ c

Alias of le_trans'.

theorem LE.le.trans_lt {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

a ≤ b → b < c → a < c

Alias of lt_of_le_of_lt.

theorem LE.le.trans_lt' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a < b → a < c

Alias of lt_of_le_of_lt'.

theorem LE.le.antisymm {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≤ a → a = b

Alias of le_antisymm.

theorem LE.le.antisymm' {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≤ a → b = a

Alias of ge_antisymm.

theorem LE.le.lt_of_ne {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → a ≠ b → a < b

Alias of lt_of_le_of_ne.

theorem LE.le.lt_of_ne' {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≠ a → a < b

Alias of lt_of_le_of_ne'.

theorem LE.le.lt_of_not_le {α : Type u} [Preorder α] {a : α} {b : α} :

a ≤ b → ¬b ≤ a → a < b

Alias of lt_of_le_not_le.

theorem LE.le.lt_or_eq {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b → a < b ∨ a = b

Alias of lt_or_eq_of_le.

theorem LE.le.lt_or_eq_dec {α : Type u} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} (hab : a ≤ b) :

a < b ∨ a = b

Alias of Decidable.lt_or_eq_of_le.

theorem LT.lt.le {α : Type u} [Preorder α] {a : α} {b : α} :

a < b → a ≤ b

Alias of le_of_lt.

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

a < b → b < c → a < c

Alias of lt_trans.

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

b < c → a < b → a < c

Alias of lt_trans'.

theorem LT.lt.trans_le {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

a < b → b ≤ c → a < c

Alias of lt_of_lt_of_le.

theorem LT.lt.trans_le' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b < c → a ≤ b → a < c

Alias of lt_of_lt_of_le'.

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

a ≠ b

Alias of ne_of_lt.

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

¬b < a

Alias of lt_asymm.

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

¬b < a

Alias of lt_asymm.

theorem Eq.le {α : Type u} [Preorder α] {a : α} {b : α} :

a = b → a ≤ b

Alias of le_of_eq.

theorem le_rfl {α : Type u} [Preorder α] {a : α} :

a ≤ a

A version of le_refl where the argument is implicit

@[simp]

theorem lt_self_iff_false {α : Type u} [Preorder α] (x : α) :

x < x ↔ False

theorem le_of_le_of_eq' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a = b → a ≤ c

theorem le_of_eq_of_le' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b = c → a ≤ b → a ≤ c

theorem lt_of_lt_of_eq' {α : Type u} [Preorder α] {a : α} {b : α} {c : α} :

b < c → a = b → a < c

theorem lt_of_eq_of_lt' {α : Type u} [Preorder α] {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} [Preorder α] {a : α} {b : α} {c : α} :

b ≤ c → a = b → a ≤ 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} [Preorder α] {a : α} {b : α} {c : α} :

b < c → a = b → a < 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} [Preorder α] {a : α} {b : α} {c : α} :

b = c → a ≤ b → a ≤ 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} [Preorder α] {a : α} {b : α} {c : α} :

b = c → a < b → a < c

Alias of lt_of_eq_of_lt'.

theorem Eq.ge {α : Type u} [Preorder α] {x : α} {y : α} (h : x = y) :

y ≤ x

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 Eq.not_lt {α : Type u} [Preorder α] {x : α} {y : α} (h : x = y) :

¬x < y

theorem Eq.not_gt {α : Type u} [Preorder α] {x : α} {y : α} (h : x = y) :

¬y < x

@[simp]

theorem le_of_subsingleton {α : Type u} [Preorder α] {a : α} {b : α} [Subsingleton α] :

a ≤ b

theorem not_lt_of_subsingleton {α : Type u} [Preorder α] {a : α} {b : α} [Subsingleton α] :

¬a < b

theorem LE.le.ge {α : Type u} [LE α] {x : α} {y : α} (h : x ≤ y) :

y ≥ x

theorem LE.le.lt_iff_ne {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a < b ↔ a ≠ b

theorem LE.le.gt_iff_ne {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a < b ↔ b ≠ a

theorem LE.le.not_lt_iff_eq {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

¬a < b ↔ a = b

theorem LE.le.not_gt_iff_eq {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

¬a < b ↔ b = a

theorem LE.le.le_iff_eq {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

b ≤ a ↔ b = a

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

b ≤ a ↔ a = b

theorem LE.le.lt_or_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a < c ∨ c ≤ b

theorem LE.le.le_or_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a ≤ c ∨ c < b

theorem LE.le.le_or_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) (c : α) :

a ≤ c ∨ c ≤ b

theorem LT.lt.gt {α : Type u} [LT α] {x : α} {y : α} (h : x < y) :

y > x

theorem LT.lt.false {α : Type u} [Preorder α] {x : α} :

x < x → False

theorem LT.lt.ne' {α : Type u} [Preorder α] {x : α} {y : α} (h : x < y) :

y ≠ x

theorem LT.lt.lt_or_lt {α : Type u} [LinearOrder α] {x : α} {y : α} (h : x < y) (z : α) :

x < z ∨ z < y

theorem GE.ge.le {α : Type u} [LE α] {x : α} {y : α} (h : x ≥ y) :

y ≤ x

theorem GT.gt.lt {α : Type u} [LT α] {x : α} {y : α} (h : x > y) :

y < x

theorem ge_of_eq {α : Type u} [Preorder α] {a : α} {b : α} (h : a = b) :

a ≥ b

theorem not_le_of_lt {α : Type u} [Preorder α] {a : α} {b : α} (h : a < b) :

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

Alias of not_le_of_lt.

theorem not_lt_of_le {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) :

¬b < a

theorem LE.le.not_lt {α : Type u} [Preorder α] {a : α} {b : α} (h : a ≤ b) :

¬b < a

Alias of not_lt_of_le.

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

a ≠ b

theorem Decidable.le_iff_eq_or_lt {α : Type u} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem le_iff_eq_or_lt {α : Type u} [PartialOrder α] {a : α} {b : α} :

a ≤ b ↔ a = b ∨ a < b

theorem lt_iff_le_and_ne {α : Type u} [PartialOrder α] {a : α} {b : α} :

a < b ↔ a ≤ b ∧ a ≠ b

theorem eq_iff_not_lt_of_le {α : Type u_3} [PartialOrder α] {x : α} {y : α} :

x ≤ y → y = x ↔ ¬x < y

theorem Decidable.eq_iff_le_not_lt {α : Type u} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_iff_le_not_lt {α : Type u} [PartialOrder α] {a : α} {b : α} :

a = b ↔ a ≤ b ∧ ¬a < b

theorem eq_or_lt_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a = b ∨ a < b

theorem eq_or_gt_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

b = a ∨ a < b

theorem gt_or_eq_of_le {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≤ b) :

a < b ∨ b = a

theorem LE.le.eq_or_lt_dec {α : Type u} [PartialOrder α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} (hab : a ≤ b) :

a = b ∨ a < b

Alias of Decidable.eq_or_lt_of_le.

theorem LE.le.eq_or_lt {α : Type u} [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} [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} [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} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) (hba : ¬a < b) :

a = b

theorem eq_of_ge_of_not_gt {α : Type u} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) (hba : ¬a < b) :

b = a

theorem LE.le.eq_of_not_lt {α : Type u} [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} [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} [PartialOrder α] {a : α} {b : α} (h : a ≠ b) :

a ≤ b ↔ a < b

theorem Ne.not_le_or_not_le {α : Type u} [PartialOrder α] {a : α} {b : α} (h : a ≠ b) :

¬a ≤ b ∨ ¬b ≤ a

theorem Decidable.ne_iff_lt_iff_le {α : Type u} [PartialOrder α] [DecidableEq α] {a : α} {b : α} :

(a ≠ b ↔ a < b) ↔ a ≤ b

@[simp]

theorem ne_iff_lt_iff_le {α : Type u} [PartialOrder α] {a : α} {b : α} :

(a ≠ b ↔ a < b) ↔ a ≤ b

theorem min_def' {α : Type u} [LinearOrder α] (a : α) (b : α) :

min a b = if b ≤ a then b else a

theorem max_def' {α : Type u} [LinearOrder α] (a : α) (b : α) :

max a b = if b ≤ a then a else b

theorem lt_of_not_le {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ¬b ≤ a) :

a < b

theorem lt_iff_not_le {α : Type u} [LinearOrder α] {x : α} {y : α} :

x < y ↔ ¬y ≤ x

theorem Ne.lt_or_lt {α : Type u} [LinearOrder α] {x : α} {y : α} (h : x ≠ y) :

x < y ∨ y < x

@[simp]

theorem lt_or_lt_iff_ne {α : Type u} [LinearOrder α] {x : α} {y : α} :

x < y ∨ y < x ↔ x ≠ y

A version of ne_iff_lt_or_gt with LHS and RHS reversed.

theorem not_lt_iff_eq_or_lt {α : Type u} [LinearOrder α] {a : α} {b : α} :

¬a < b ↔ a = b ∨ b < a

theorem exists_ge_of_linear {α : Type u} [LinearOrder α] (a : α) (b : α) :

∃ (c : α), a ≤ c ∧ b ≤ c

theorem lt_imp_lt_of_le_imp_le {α : Type u} {β : Type u_3} [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} {β : Type u_3} [LinearOrder α] [LinearOrder β] {a : α} {b : α} {c : β} {d : β} :

a ≤ b → c ≤ d ↔ d < c → b < a

theorem lt_iff_lt_of_le_iff_le' {α : Type u} {β : Type u_3} [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} {β : Type u_3} [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} {β : Type u_3} [LinearOrder α] [LinearOrder β] {a : α} {b : α} {c : β} {d : β} :

(a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c)

theorem eq_of_forall_le_iff {α : Type u} [PartialOrder α] {a : α} {b : α} (H : ∀ (c : α), c ≤ a ↔ c ≤ b) :

a = b

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

a ≤ b

theorem le_of_forall_le' {α : Type u} [Preorder α] {a : α} {b : α} (H : ∀ (c : α), a ≤ c → b ≤ c) :

b ≤ a

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

a ≤ b

theorem forall_lt_iff_le {α : Type u} [LinearOrder α] {a : α} {b : α} :

(∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b

theorem le_of_forall_lt' {α : Type u} [LinearOrder α] {a : α} {b : α} (H : ∀ (c : α), a < c → b < c) :

b ≤ a

theorem forall_lt_iff_le' {α : Type u} [LinearOrder α] {a : α} {b : α} :

(∀ ⦃c : α⦄, a < c → b < c) ↔ b ≤ a

theorem eq_of_forall_ge_iff {α : Type u} [PartialOrder α] {a : α} {b : α} (H : ∀ (c : α), a ≤ c ↔ b ≤ c) :

a = b

theorem eq_of_forall_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), c < a ↔ c < b) :

a = b

theorem eq_of_forall_gt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} (h : ∀ (c : α), a < c ↔ b < c) :

a = b

theorem rel_imp_eq_of_rel_imp_le {α : Type u} {β : Type v} [PartialOrder β] (r : α → α → Prop) [IsSymm α 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.

theorem le_implies_le_of_le_of_le {α : Type u} {a : α} {b : α} {c : α} {d : α} [Preorder α] (hca : c ≤ a) (hbd : b ≤ d) :

a ≤ b → c ≤ d

monotonicity of ≤ with respect to →

theorem commutative_of_le {α : Type u} {β : Type v} [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} [PartialOrder α] {f : α → α → α} (comm : 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 Preorder.toLE_injective {α : Type u_3} :

Function.Injective (@Preorder.toLE α)

theorem PartialOrder.toPreorder_injective {α : Type u_3} :

Function.Injective (@PartialOrder.toPreorder α)

theorem LinearOrder.toPartialOrder_injective {α : Type u_3} :

Function.Injective (@LinearOrder.toPartialOrder α)

theorem Preorder.ext {α : Type u_3} {A : Preorder α} {B : Preorder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

theorem PartialOrder.ext {α : Type u_3} {A : PartialOrder α} {B : PartialOrder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

theorem LinearOrder.ext {α : Type u_3} {A : LinearOrder α} {B : LinearOrder α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

def Order.Preimage {α : Sort u_3} {β : Sort u_4} (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

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

Instances For

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

Instances For

instance Order.Preimage.decidable {α : Sort u_3} {β : Sort u_4} (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)

@[simp]

theorem ltByCases_lt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :

ltByCases x y h₁ h₂ h₃ = h₁ h

@[simp]

theorem ltByCases_gt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :

ltByCases x y h₁ h₂ h₃ = h₃ h

@[simp]

theorem ltByCases_eq {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :

ltByCases x y h₁ h₂ h₃ = h₂ h

theorem ltByCases_not_lt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : ¬x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : optParam (¬y < x → x = y) (_ : ¬y < x → x = y)) :

ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂ (_ : x = y)

theorem ltByCases_not_gt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : ¬y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : optParam (¬x < y → x = y) (_ : ¬x < y → x = y)) :

ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂ (_ : x = y)

theorem ltByCases_ne {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} (h : x ≠ y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : optParam (¬x < y → y < x) (_ : ¬x < y → y < x)) :

ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃ (_ : y < x)

theorem ltByCases_comm {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : optParam (y = x → x = y) (_ : y = x → x = 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} [LinearOrder α] {x : α} {y : α} {x' : α} {y' : α} (ltc : x < y ↔ x' < y') (gtc : y < x ↔ y' < x') :

x = y ↔ x' = y'

theorem ltByCases_rec {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (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

theorem ltByCases_eq_iff {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {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

theorem ltByCases_congr {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {x' : α} {y' : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {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₁ (_ : x < y) = h₁' h) (hh'₂ : ∀ (h : x' = y'), h₂ (_ : x = y) = h₂' h) (hh'₃ : ∀ (h : y' < x'), h₃ (_ : y < x) = h₃' h) :

ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃'

@[inline, reducible]

abbrev ltTrichotomy {α : Type u} [LinearOrder α] {P : Sort u_3} (x : α) (y : α) (p : P) (q : P) (r : P) :

P

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

Equations

ltTrichotomy x y p q r = ltByCases x y (fun (x : x < y) => p) (fun (x : x = y) => q) fun (x : y < x) => r

Instances For

@[simp]

theorem ltTrichotomy_lt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : x < y) :

ltTrichotomy x y p q r = p

@[simp]

theorem ltTrichotomy_gt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : y < x) :

ltTrichotomy x y p q r = r

@[simp]

theorem ltTrichotomy_eq {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : x = y) :

ltTrichotomy x y p q r = q

theorem ltTrichotomy_not_lt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : ¬x < y) :

ltTrichotomy x y p q r = if y < x then r else q

theorem ltTrichotomy_not_gt {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : ¬y < x) :

ltTrichotomy x y p q r = if x < y then p else q

theorem ltTrichotomy_ne {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} (h : x ≠ y) :

ltTrichotomy x y p q r = if x < y then p else r

theorem ltTrichotomy_comm {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} :

ltTrichotomy x y p q r = ltTrichotomy y x r q p

theorem ltTrichotomy_self {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} :

ltTrichotomy x y p p p = p

theorem ltTrichotomy_eq_iff {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} {s : P} :

ltTrichotomy x y p q r = s ↔ x < y ∧ p = s ∨ x = y ∧ q = s ∨ y < x ∧ r = s

theorem ltTrichotomy_congr {α : Type u} [LinearOrder α] {P : Sort u_3} {x : α} {y : α} {p : P} {q : P} {r : P} {x' : α} {y' : α} {p' : P} {q' : P} {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'

Order dual #

def OrderDual (α : Type u_3) :

Type u_3

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

Equations

αᵒᵈ = α

Instances For

def «term_ᵒᵈ» :

Lean.TrailingParserDescr

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

Equations

«term_ᵒᵈ» = Lean.ParserDescr.trailingNode `term_ᵒᵈ 1024 0 (Lean.ParserDescr.symbol "ᵒᵈ")

Instances For

instance OrderDual.instNonemptyOrderDual (α : Type u_3) [h : Nonempty α] :

Nonempty αᵒᵈ

Equations

(_ : Nonempty αᵒᵈ) = h

instance OrderDual.instSubsingletonOrderDual (α : Type u_3) [h : Subsingleton α] :

Subsingleton αᵒᵈ

Equations

(_ : Subsingleton αᵒᵈ) = h

instance OrderDual.instLEOrderDual (α : Type u_3) [LE α] :

Equations

OrderDual.instLEOrderDual α = { le := fun (x y : α) => y ≤ x }

instance OrderDual.instLTOrderDual (α : Type u_3) [LT α] :

Equations

OrderDual.instLTOrderDual α = { lt := fun (x y : α) => y < x }

instance OrderDual.instPreorder (α : Type u_3) [Preorder α] :

Preorder αᵒᵈ

Equations

OrderDual.instPreorder α = Preorder.mk (_ : ∀ (x : αᵒᵈ), x ≤ x) (_ : ∀ (x x_1 x_2 : αᵒᵈ), x ≤ x_1 → x_1 ≤ x_2 → x_2 ≤ x)

instance OrderDual.instPartialOrder (α : Type u_3) [PartialOrder α] :

PartialOrder αᵒᵈ

Equations

OrderDual.instPartialOrder α = let src := inferInstanceAs (Preorder αᵒᵈ); PartialOrder.mk (_ : ∀ (a b : αᵒᵈ), a ≤ b → b ≤ a → a = b)

instance OrderDual.instLinearOrder (α : Type u_3) [LinearOrder α] :

LinearOrder αᵒᵈ

Equations

OrderDual.instLinearOrder α = let src := inferInstanceAs (PartialOrder αᵒᵈ); LinearOrder.mk (_ : ∀ (a b : α), b ≤ a ∨ a ≤ b) inferInstance decidableEqOfDecidableLE inferInstance

instance OrderDual.instForAllInhabitedOrderDual {α : Type u} [Inhabited α] :

Inhabited αᵒᵈ

Equations

OrderDual.instForAllInhabitedOrderDual = x

theorem OrderDual.Preorder.dual_dual (α : Type u_3) [H : Preorder α] :

OrderDual.instPreorder αᵒᵈ = H

theorem OrderDual.instPartialOrder.dual_dual (α : Type u_3) [H : PartialOrder α] :

OrderDual.instPartialOrder αᵒᵈ = H

theorem OrderDual.instLinearOrder.dual_dual (α : Type u_3) [H : LinearOrder α] :

OrderDual.instLinearOrder αᵒᵈ = H

`HasCompl` #

instance Prop.hasCompl :

Equations

Prop.hasCompl = { compl := Not }

instance Pi.hasCompl {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] :

HasCompl ((i : ι) → α i)

Equations

Pi.hasCompl = { compl := fun (x : (i : ι) → α i) (i : ι) => (x i)ᶜ }

theorem Pi.compl_def {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] (x : (i : ι) → α i) :

xᶜ = fun (i : ι) => (x i)ᶜ

@[simp]

theorem Pi.compl_apply {ι : Type u} {α : ι → Type v} [(i : ι) → HasCompl (α i)] (x : (i : ι) → α i) (i : ι) :

x ᶜ i = (x i)ᶜ

instance IsIrrefl.compl {α : Type u} (r : α → α → Prop) [IsIrrefl α r] :

Equations

(_ : IsRefl α rᶜ) = (_ : IsRefl α rᶜ)

instance IsRefl.compl {α : Type u} (r : α → α → Prop) [IsRefl α r] :

IsIrrefl α rᶜ

Equations

(_ : IsIrrefl α rᶜ) = (_ : IsIrrefl α rᶜ)

Order instances on the function space #

instance Pi.hasLe {ι : Type u} {α : ι → Type v} [(i : ι) → LE (α i)] :

LE ((i : ι) → α i)

Equations

Pi.hasLe = { le := fun (x y : (i : ι) → α i) => ∀ (i : ι), x i ≤ y i }

theorem Pi.le_def {ι : Type u} {α : ι → Type v} [(i : ι) → LE (α i)] {x : (i : ι) → α i} {y : (i : ι) → α i} :

x ≤ y ↔ ∀ (i : ι), x i ≤ y i

instance Pi.preorder {ι : Type u} {α : ι → Type v} [(i : ι) → Preorder (α i)] :

Preorder ((i : ι) → α i)

Equations

Pi.preorder = let src := inferInstanceAs (LE ((i : ι) → α i)); Preorder.mk (_ : ∀ (a : (i : ι) → α i) (i : ι), a i ≤ a i) (_ : ∀ (a b c : (i : ι) → α i), a ≤ b → b ≤ c → ∀ (i : ι), a i ≤ c i)

theorem Pi.lt_def {ι : Type u} {α : ι → Type v} [(i : ι) → Preorder (α i)] {x : (i : ι) → α i} {y : (i : ι) → α i} :

x < y ↔ x ≤ y ∧ ∃ (i : ι), x i < y i

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

PartialOrder ((i : ι) → π i)

Equations

Pi.partialOrder = let src := Pi.preorder; PartialOrder.mk (_ : ∀ (x x_1 : (i : ι) → π i), x ≤ x_1 → x_1 ≤ x → x = x_1)

def StrongLT {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → LT (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) :

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

Instances For

theorem le_of_strongLT {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} (h : StrongLT a b) :

a ≤ b

theorem lt_of_strongLT {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} [Nonempty ι] (h : StrongLT a b) :

a < b

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

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

theorem StrongLT.le {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} (h : StrongLT a b) :

a ≤ b

Alias of le_of_strongLT.

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

a < b

Alias of lt_of_strongLT.

theorem StrongLT.trans_le {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {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_2} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} {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_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {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_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} :

Function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j : ι), j ≠ i → x j ≤ y j

theorem update_le_update_iff {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} {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_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {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_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {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_2} [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_2} [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_2} [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_2} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :

Function.update x i a < x ↔ a < x i

instance Pi.sdiff {ι : Type u} {α : ι → Type v} [(i : ι) → SDiff (α i)] :

SDiff ((i : ι) → α i)

Equations

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

theorem Pi.sdiff_def {ι : Type u} {α : ι → Type v} [(i : ι) → SDiff (α i)] (x : (i : ι) → α i) (y : (i : ι) → α i) :

x \ y = fun (i : ι) => x i \ y i

@[simp]

theorem Pi.sdiff_apply {ι : Type u} {α : ι → Type v} [(i : ι) → SDiff (α i)] (x : (i : ι) → α i) (y : (i : ι) → α i) (i : ι) :

(x \ y) i = x i \ y i

@[simp]

theorem Function.const_le_const {α : Type u} {β : Type v} [Preorder α] [Nonempty β] {a : α} {b : α} :

Function.const β a ≤ Function.const β b ↔ a ≤ b

@[simp]

theorem Function.const_lt_const {α : Type u} {β : Type v} [Preorder α] [Nonempty β] {a : α} {b : α} :

Function.const β a < Function.const β b ↔ a < b

`min`/`max` recursors #

theorem min_rec {α : Type u} [LinearOrder α] {p : α → Prop} {x : α} {y : α} (hx : x ≤ y → p x) (hy : y ≤ x → p y) :

p (min x y)

theorem max_rec {α : Type u} [LinearOrder α] {p : α → Prop} {x : α} {y : α} (hx : y ≤ x → p x) (hy : x ≤ y → p y) :

p (max x y)

theorem min_rec' {α : Type u} [LinearOrder α] {x : α} {y : α} (p : α → Prop) (hx : p x) (hy : p y) :

p (min x y)

theorem max_rec' {α : Type u} [LinearOrder α] {x : α} {y : α} (p : α → Prop) (hx : p x) (hy : p y) :

p (max x y)

theorem min_def_lt {α : Type u} [LinearOrder α] (x : α) (y : α) :

min x y = if x < y then x else y

theorem max_def_lt {α : Type u} [LinearOrder α] (x : α) (y : α) :

max x y = if x < y then y else x

Lifts of order instances #

@[reducible]

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

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

Equations

Preorder.lift f = Preorder.mk (_ : ∀ (x : α), f x ≤ f x) (_ : ∀ (x x_1 x_2 : α), f x ≤ f x_1 → f x_1 ≤ f x_2 → f x ≤ f x_2)

Instances For

@[reducible]

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

PartialOrder α

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

Equations

PartialOrder.lift f inj = let src := Preorder.lift f; PartialOrder.mk (_ : ∀ (x x_1 : α), x ≤ x_1 → x_1 ≤ x → x = x_1)

Instances For

theorem compare_of_injective_eq_compareOfLessAndEq {α : Type u} {β : Type v} (a : α) (b : α) [LinearOrder β] [DecidableEq α] (f : α → β) (inj : Function.Injective f) [Decidable (a < b)] :

compare (f a) (f b) = compareOfLessAndEq a b

@[reducible]

def LinearOrder.lift {α : Type u_3} {β : Type u_4} [LinearOrder β] [Sup α] [Inf α] (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)) :

Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Sup α] and [Inf α] 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

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

Instances For

@[reducible]

def LinearOrder.lift' {α : Type u_3} {β : Type u_4} [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 [Sup α] and [Inf α], 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

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

Instances For

@[reducible]

def LinearOrder.liftWithOrd {α : Type u_3} {β : Type u_4} [LinearOrder β] [Sup α] [Inf α] [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)) :

Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version takes [Sup α] and [Inf α] 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

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

Instances For

@[reducible]

def LinearOrder.liftWithOrd' {α : Type u_3} {β : Type u_4} [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

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

Instances For

Subtype of an order #

instance Subtype.le {α : Type u} [LE α] {p : α → Prop} :

Equations

Subtype.le = { le := fun (x y : Subtype p) => ↑x ≤ ↑y }

instance Subtype.lt {α : Type u} [LT α] {p : α → Prop} :

Equations

Subtype.lt = { lt := fun (x y : Subtype p) => ↑x < ↑y }

@[simp]

theorem Subtype.mk_le_mk {α : Type u} [LE α] {p : α → Prop} {x : α} {y : α} {hx : p x} {hy : p y} :

{ val := x, property := hx } ≤ { val := y, property := hy } ↔ x ≤ y

@[simp]

theorem Subtype.mk_lt_mk {α : Type u} [LT α] {p : α → Prop} {x : α} {y : α} {hx : p x} {hy : p y} :

{ val := x, property := hx } < { val := y, property := hy } ↔ x < y

@[simp]

theorem Subtype.coe_le_coe {α : Type u} [LE α] {p : α → Prop} {x : Subtype p} {y : Subtype p} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem Subtype.coe_lt_coe {α : Type u} [LT α] {p : α → Prop} {x : Subtype p} {y : Subtype p} :

↑x < ↑y ↔ x < y

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

Preorder (Subtype p)

Equations

Subtype.preorder p = Preorder.lift fun (a : Subtype p) => ↑a

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

PartialOrder (Subtype p)

Equations

Subtype.partialOrder p = PartialOrder.lift (fun (a : Subtype p) => ↑a) (_ : Function.Injective fun (a : Subtype p) => ↑a)

instance Subtype.decidableLE {α : Type u} [Preorder α] [h : DecidableRel fun (x x_1 : α) => x ≤ x_1] {p : α → Prop} :

DecidableRel fun (x x_1 : Subtype p) => x ≤ x_1

Equations

Subtype.decidableLE a b = h ↑a ↑b

instance Subtype.decidableLT {α : Type u} [Preorder α] [h : DecidableRel fun (x x_1 : α) => x < x_1] {p : α → Prop} :

DecidableRel fun (x x_1 : Subtype p) => x < x_1

Equations

Subtype.decidableLT a b = h ↑a ↑b

instance Subtype.linearOrder {α : Type u} [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 Prod.instLEProd (α : Type u) (β : Type v) [LE α] [LE β] :

LE (α × β)

Equations

Prod.instLEProd α β = { le := fun (p q : α × β) => p.1 ≤ q.1 ∧ p.2 ≤ q.2 }

instance Prod.instDecidableLE (α : Type u) (β : Type v) [LE α] [LE β] (x : α × β) (y : α × β) [Decidable (x.1 ≤ y.1)] [Decidable (x.2 ≤ y.2)] :

Decidable (x ≤ y)

Equations

Prod.instDecidableLE α β x y = And.decidable

theorem Prod.le_def {α : Type u} {β : Type v} [LE α] [LE β] {x : α × β} {y : α × β} :

x ≤ y ↔ x.1 ≤ y.1 ∧ x.2 ≤ y.2

@[simp]

theorem Prod.mk_le_mk {α : Type u} {β : Type v} [LE α] [LE β] {x₁ : α} {x₂ : α} {y₁ : β} {y₂ : β} :

(x₁, y₁) ≤ (x₂, y₂) ↔ x₁ ≤ x₂ ∧ y₁ ≤ y₂

@[simp]

theorem Prod.swap_le_swap {α : Type u} {β : Type v} [LE α] [LE β] {x : α × β} {y : α × β} :

Prod.swap x ≤ Prod.swap y ↔ x ≤ y

instance Prod.instPreorderProd (α : Type u) (β : Type v) [Preorder α] [Preorder β] :

Preorder (α × β)

Equations

Prod.instPreorderProd α β = let src := inferInstanceAs (LE (α × β)); Preorder.mk (_ : ∀ (x : α × β), x ≤ x) (_ : ∀ (x x_1 x_2 : α × β), x ≤ x_1 → x_1 ≤ x_2 → x ≤ x_2)

@[simp]

theorem Prod.swap_lt_swap {α : Type u} {β : Type v} [Preorder α] [Preorder β] {x : α × β} {y : α × β} :

Prod.swap x < Prod.swap y ↔ x < y

theorem Prod.mk_le_mk_iff_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {a₁ : α} {a₂ : α} {b : β} :

(a₁, b) ≤ (a₂, b) ↔ a₁ ≤ a₂

theorem Prod.mk_le_mk_iff_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {a : α} {b₁ : β} {b₂ : β} :

(a, b₁) ≤ (a, b₂) ↔ b₁ ≤ b₂

theorem Prod.mk_lt_mk_iff_left {α : Type u} {β : Type v} [Preorder α] [Preorder β] {a₁ : α} {a₂ : α} {b : β} :

(a₁, b) < (a₂, b) ↔ a₁ < a₂

theorem Prod.mk_lt_mk_iff_right {α : Type u} {β : Type v} [Preorder α] [Preorder β] {a : α} {b₁ : β} {b₂ : β} :

(a, b₁) < (a, b₂) ↔ b₁ < b₂

theorem Prod.lt_iff {α : Type u} {β : Type v} [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} {β : Type v} [Preorder α] [Preorder β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :

(a₁, b₁) < (a₂, b₂) ↔ a₁ < a₂ ∧ b₁ ≤ b₂ ∨ a₁ ≤ a₂ ∧ b₁ < b₂

instance Prod.instPartialOrder (α : Type u) (β : Type v) [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 α β = let src := inferInstanceAs (Preorder (α × β)); PartialOrder.mk (_ : ∀ (x x_1 : α × β), x ≤ x_1 → x_1 ≤ x → x = x_1)

Additional order classes #

class DenselyOrdered (α : Type u) [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} [LT α] [DenselyOrdered α] {a₁ : α} {a₂ : α} :

a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂

instance OrderDual.denselyOrdered (α : Type u) [LT α] [h : DenselyOrdered α] :

DenselyOrdered αᵒᵈ

Equations

(_ : DenselyOrdered αᵒᵈ) = (_ : DenselyOrdered αᵒᵈ)

@[simp]

theorem denselyOrdered_orderDual {α : Type u} [LT α] :

DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

instance instDenselyOrderedProdToLTInstPreorderProd {α : Type u} {β : Type v} [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :

DenselyOrdered (α × β)

Equations

(_ : DenselyOrdered (α × β)) = (_ : DenselyOrdered (α × β))

instance instDenselyOrderedForAllToLTPreorder {ι : Type u_1} {α : ι → Type u_3} [(i : ι) → Preorder (α i)] [∀ (i : ι), DenselyOrdered (α i)] :

DenselyOrdered ((i : ι) → α i)

Equations

(_ : DenselyOrdered ((i : ι) → α i)) = (_ : DenselyOrdered ((i : ι) → α i))

theorem le_of_forall_le_of_dense {α : Type u} [LinearOrder α] [DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a : α), a₂ < a → a₁ ≤ a) :

a₁ ≤ a₂

theorem eq_of_le_of_forall_le_of_dense {α : Type u} [LinearOrder α] [DenselyOrdered α] {a₁ : α} {a₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : ∀ (a : α), a₂ < a → a₁ ≤ a) :

a₁ = a₂

theorem le_of_forall_ge_of_dense {α : Type u} [LinearOrder α] [DenselyOrdered α] {a₁ : α} {a₂ : α} (h : ∀ (a₃ : α), a₃ < a₁ → a₃ ≤ a₂) :

a₁ ≤ a₂

theorem eq_of_le_of_forall_ge_of_dense {α : Type u} [LinearOrder α] [DenselyOrdered α] {a₁ : α} {a₂ : α} (h₁ : a₂ ≤ a₁) (h₂ : ∀ (a₃ : α), a₃ < a₁ → a₃ ≤ a₂) :

a₁ = a₂

theorem dense_or_discrete {α : Type u} [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} [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.

instance PUnit.linearOrder :

LinearOrder PUnit.{u_3 + 1}

Equations

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

theorem PUnit.max_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

max a b = PUnit.unit

theorem PUnit.min_eq (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

min a b = PUnit.unit

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

a ≤ b

theorem PUnit.not_lt (a : PUnit.{u + 1} ) (b : PUnit.{u + 1} ) :

¬a < b

instance PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder :

DenselyOrdered PUnit.{u_3 + 1}

Equations

PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder = (_ : DenselyOrdered PUnit.{u_3 + 1} )

instance Prop.le :

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

Equations

Prop.le = { le := fun (x x_1 : Prop) => x → x_1 }

@[simp]

theorem le_Prop_eq :

(fun (x x_1 : Prop) => x ≤ x_1) = fun (x x_1 : Prop) => x → x_1

theorem subrelation_iff_le {α : Type u} {r : α → α → Prop} {s : α → α → Prop} :

Subrelation r s ↔ r ≤ s

instance Prop.partialOrder :

PartialOrder Prop

Equations

Prop.partialOrder = let src := Prop.le; PartialOrder.mk Prop.partialOrder.proof_2

Linear order from a total partial order #

def AsLinearOrder (α : Type u) :

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

Equations

AsLinearOrder α = α

Instances For

instance instInhabitedAsLinearOrder {α : Type u_3} [Inhabited α] :

Inhabited (AsLinearOrder α)

Equations

instInhabitedAsLinearOrder = { default := default }

noncomputable instance AsLinearOrder.linearOrder {α : Type u_3} [PartialOrder α] [IsTotal α fun (x x_1 : α) => x ≤ x_1] :

LinearOrder (AsLinearOrder α)

Equations

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

theorem dite_nonneg {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), 0 ≤ a h) (hb : ∀ (h : ¬p), 0 ≤ b h) :

0 ≤ dite p a b

theorem one_le_dite {α : Type u} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), 1 ≤ a h) (hb : ∀ (h : ¬p), 1 ≤ b h) :

1 ≤ dite p a b

theorem dite_nonpos {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), a h ≤ 0) (hb : ∀ (h : ¬p), b h ≤ 0) :

dite p a b ≤ 0

theorem dite_le_one {α : Type u} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LE α] (ha : ∀ (h : p), a h ≤ 1) (hb : ∀ (h : ¬p), b h ≤ 1) :

dite p a b ≤ 1

theorem dite_pos {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), 0 < a h) (hb : ∀ (h : ¬p), 0 < b h) :

0 < dite p a b

theorem one_lt_dite {α : Type u} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), 1 < a h) (hb : ∀ (h : ¬p), 1 < b h) :

1 < dite p a b

theorem dite_neg {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), a h < 0) (hb : ∀ (h : ¬p), b h < 0) :

dite p a b < 0

theorem dite_lt_one {α : Type u} [One α] {p : Prop} [Decidable p] {a : p → α} {b : ¬p → α} [LT α] (ha : ∀ (h : p), a h < 1) (hb : ∀ (h : ¬p), b h < 1) :

dite p a b < 1

theorem ite_nonneg {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : α} {b : α} [LE α] (ha : 0 ≤ a) (hb : 0 ≤ b) :

0 ≤ if p then a else b

theorem one_le_ite {α : Type u} [One α] {p : Prop} [Decidable p] {a : α} {b : α} [LE α] (ha : 1 ≤ a) (hb : 1 ≤ b) :

1 ≤ if p then a else b

theorem ite_nonpos {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : α} {b : α} [LE α] (ha : a ≤ 0) (hb : b ≤ 0) :

(if p then a else b) ≤ 0

theorem ite_le_one {α : Type u} [One α] {p : Prop} [Decidable p] {a : α} {b : α} [LE α] (ha : a ≤ 1) (hb : b ≤ 1) :

(if p then a else b) ≤ 1

theorem ite_pos {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : α} {b : α} [LT α] (ha : 0 < a) (hb : 0 < b) :

0 < if p then a else b

theorem one_lt_ite {α : Type u} [One α] {p : Prop} [Decidable p] {a : α} {b : α} [LT α] (ha : 1 < a) (hb : 1 < b) :

1 < if p then a else b

theorem ite_neg {α : Type u} [Zero α] {p : Prop} [Decidable p] {a : α} {b : α} [LT α] (ha : a < 0) (hb : b < 0) :

(if p then a else b) < 0

theorem ite_lt_one {α : Type u} [One α] {p : Prop} [Decidable p] {a : α} {b : α} [LT α] (ha : a < 1) (hb : b < 1) :

(if p then a else b) < 1