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

b ≤ c → a ≤ b → a ≤ c

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

b < c → a < b → a < c

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

b ≤ c → a < b → a < c

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

b < c → a ≤ b → a < c

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

a ≤ b → b ≤ a → b = a

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

a ≤ b → b ≠ a → a < b

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 : α} :

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

b ≤ c → a ≤ b → a ≤ c

Alias of le_trans'.

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

a < c

Alias of lt_of_le_of_lt.

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

b ≤ c → a < b → a < c

Alias of lt_of_le_of_lt'.

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_2} [PartialOrder α] {a : α} {b : α} :

a ≤ b → b ≤ a → b = a

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

a < b

Alias of lt_of_le_not_le.

theorem LE.le.lt_or_eq {α : 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_dec {α : Type u_1} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) :

a < b ∨ a = b

Alias of Decidable.lt_or_eq_of_le.

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

a ≤ b

Alias of le_of_lt.

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

a < c

Alias of lt_trans.

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

b < c → a < b → a < c

Alias of lt_trans'.

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

a < c

Alias of lt_of_lt_of_le.

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

b < c → a ≤ b → a < c

Alias of lt_of_lt_of_le'.

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

a ≠ b

Alias of ne_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_lt {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a < b) :

¬b < a

Alias of lt_asymm.

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

a ≤ b

Alias of le_of_eq.

@[simp]

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

x < x ↔ False

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

b ≤ c → a = b → a ≤ c

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

b = c → a ≤ b → a ≤ c

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

b < c → a = b → a < c

theorem lt_of_eq_of_lt' {α : Type u_2} [Preorder α] {a : α} {b : α} {c : α} :

b = c → a < b → a < c

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

a ≤ c

Alias of le_of_le_of_eq.

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

b ≤ c → a = b → a ≤ c

Alias of le_of_le_of_eq'.

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

a < c

Alias of lt_of_lt_of_eq.

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

b < c → a = b → a < c

Alias of lt_of_lt_of_eq'.

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

a ≤ c

Alias of le_of_eq_of_le.

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

b = c → a ≤ b → a ≤ c

Alias of le_of_eq_of_le'.

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

a < c

Alias of lt_of_eq_of_lt.

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

b = c → a < b → a < c

Alias of lt_of_eq_of_lt'.

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

¬x < y

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

¬y < x

@[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.le.ge {α : Type u_2} [LE α] {x : α} {y : α} (h : x ≤ y) :

y ≥ x

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

a < b ↔ a ≠ b

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

a < b ↔ b ≠ a

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

¬a < b ↔ a = b

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

¬a < b ↔ b = a

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

b ≤ a ↔ b = a

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

b ≤ a ↔ a = b

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

a < c ∨ c ≤ b

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

a ≤ c ∨ c < b

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

a ≤ c ∨ c ≤ b

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

y > x

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

x < x → False

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

y ≠ x

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

x < z ∨ z < y

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

y ≤ x

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

y < x

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

a ≥ b

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

a ≠ b

theorem Decidable.le_iff_eq_or_lt {α : Type u_2} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] :

a ≤ b ↔ a = b ∨ a < b

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

a ≤ b ↔ a = b ∨ a < b

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

a < b ↔ a ≤ b ∧ a ≠ b

theorem eq_iff_not_lt_of_le {α : Type u_2} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) :

a = b ↔ ¬a < b

theorem LE.le.eq_iff_not_lt {α : Type u_2} [PartialOrder α] {a : α} {b : α} (hab : a ≤ b) :

a = b ↔ ¬a < b

Alias of eq_iff_not_lt_of_le.

theorem Decidable.eq_iff_le_not_lt {α : Type u_2} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] :

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

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

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

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

a = b ∨ a < b

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

b = a ∨ a < b

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

a < b ∨ b = a

theorem LE.le.eq_or_lt_dec {α : Type u_1} [PartialOrder α] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (hab : a ≤ b) :

a = b ∨ a < b

Alias of Decidable.eq_or_lt_of_le.

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

a = b ∨ a < b

Alias of eq_or_lt_of_le.

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

b = a ∨ a < b

Alias of eq_or_gt_of_le.

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

a < b ∨ b = a

Alias of gt_or_eq_of_le.

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

a = b

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

b = a

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

a = b

Alias of eq_of_le_of_not_lt.

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

b = a

Alias of eq_of_ge_of_not_gt.

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

a ≤ b ↔ a < b

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

¬a ≤ b ∨ ¬b ≤ a

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

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

@[simp]

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

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

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

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

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

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

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

a < b

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

x < y ↔ ¬y ≤ x

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

x < y ∨ y < x

@[simp]

theorem lt_or_lt_iff_ne {α : Type u_2} [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_2} [LinearOrder α] {a : α} {b : α} :

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

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

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

theorem exists_forall_ge_and {α : Type u_2} [LinearOrder α] {p : α → Prop} {q : α → Prop} :

(∃ (i : α), ∀ (j : α), j ≥ i → p j) → (∃ (i : α), ∀ (j : α), j ≥ i → q j) → ∃ (i : α), ∀ (j : α), j ≥ i → p j ∧ q j

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

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

b ≤ a

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

a ≤ b

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

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

theorem le_of_forall_lt' {α : 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 : α⦄, a < c → b < c) ↔ b ≤ a

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

a = b

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 rel_imp_eq_of_rel_imp_le {α : Type u_2} {β : Type u_3} [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_2} {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_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 Preorder.toLE_injective_iff {α : Type u_2} {a₁ : Preorder α} {a₂ : Preorder α} :

a₁ = a₂ ↔ Preorder.toLE = Preorder.toLE

theorem Preorder.toLE_injective {α : Type u_2} :

Function.Injective (@Preorder.toLE α)

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

a₁ = a₂ ↔ PartialOrder.toPreorder = PartialOrder.toPreorder

theorem PartialOrder.toPreorder_injective {α : Type u_2} :

Function.Injective (@PartialOrder.toPreorder α)

theorem LinearOrder.toPartialOrder_injective_iff {α : Type u_2} {a₁ : LinearOrder α} {a₂ : LinearOrder α} :

a₁ = a₂ ↔ LinearOrder.toPartialOrder = LinearOrder.toPartialOrder

theorem LinearOrder.toPartialOrder_injective {α : Type u_2} :

Function.Injective (@LinearOrder.toPartialOrder α)

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

A = B

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

A = B

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

A = B

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

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

Equations

(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 {α : 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)

@[simp]

theorem ltByCases_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {x : α} {y : α} (h : ¬x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : optParam (¬y < x → x = y) ⋯) :

ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂ ⋯

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

ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂ ⋯

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

ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃ ⋯

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

x = y ↔ x' = y'

theorem ltByCases_rec {α : Type u_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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₁ ⋯ = h₁' h) (hh'₂ : ∀ (h : x' = y'), h₂ ⋯ = h₂' h) (hh'₃ : ∀ (h : y' < x'), h₃ ⋯ = h₃' h) :

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

@[reducible, inline]

abbrev ltTrichotomy {α : Type u_2} [LinearOrder α] {P : Sort u_5} (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_2} [LinearOrder α] {P : Sort u_5} {x : α} {y : α} {p : P} {q : P} {r : P} (h : x < y) :

ltTrichotomy x y p q r = p

@[simp]

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

ltTrichotomy x y p q r = r

@[simp]

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

ltTrichotomy x y p q r = q

theorem ltTrichotomy_not_lt {α : Type u_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {x : α} {y : α} {p : P} :

ltTrichotomy x y p p p = p

theorem ltTrichotomy_eq_iff {α : Type u_2} [LinearOrder α] {P : Sort u_5} {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_2} [LinearOrder α] {P : Sort u_5} {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_5) :

Type u_5

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.instNonempty (α : Type u_5) [h : Nonempty α] :

Nonempty αᵒᵈ

Equations

⋯ = h

instance OrderDual.instSubsingleton (α : Type u_5) [h : Subsingleton α] :

Subsingleton αᵒᵈ

Equations

⋯ = h

instance OrderDual.instLE (α : Type u_5) [LE α] :

Equations

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

instance OrderDual.instLT (α : Type u_5) [LT α] :

Equations

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

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

Preorder αᵒᵈ

Equations

OrderDual.instPreorder α = Preorder.mk ⋯ ⋯ ⋯

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

PartialOrder αᵒᵈ

Equations

OrderDual.instPartialOrder α = PartialOrder.mk ⋯

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

LinearOrder αᵒᵈ

Equations

OrderDual.instLinearOrder α = LinearOrder.mk ⋯ inferInstance decidableEqOfDecidableLE inferInstance ⋯ ⋯ ⋯

def LinearOrder.swap (α : Type u_5) :

LinearOrder α → LinearOrder α

The opposite linear order to a given linear order

Equations

LinearOrder.swap α x = inferInstanceAs (LinearOrder αᵒᵈ)

Instances For

instance OrderDual.instInhabited {α : Type u_2} [Inhabited α] :

Inhabited αᵒᵈ

Equations

OrderDual.instInhabited = x

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

OrderDual.instPreorder αᵒᵈ = H

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

OrderDual.instPartialOrder αᵒᵈ = H

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

OrderDual.instLinearOrder αᵒᵈ = H

`HasCompl` #

instance Prop.hasCompl :

Equations

«Prop».hasCompl = { compl := Not }

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

HasCompl ((i : ι) → π i)

Equations

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

theorem Pi.compl_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → HasCompl (π i)] (x : (i : ι) → π i) :

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

@[simp]

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

xᶜ i = (x i)ᶜ

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

Equations

⋯ = ⋯

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

IsIrrefl α rᶜ

Equations

⋯ = ⋯

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

Order instances on the function space #

instance Pi.hasLe {ι : Type u_1} {π : ι → Type u_4} [(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_1} {π : ι → Type u_4} [(i : ι) → LE (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} :

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

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

Preorder ((i : ι) → π i)

Equations

Pi.preorder = Preorder.mk ⋯ ⋯ ⋯

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

PartialOrder ((i : ι) → π i)

Equations

Pi.partialOrder = PartialOrder.mk ⋯

@[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 : (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_4} [(i : ι) → Preorder (π i)] {a : (i : ι) → π i} {b : (i : ι) → π i} (h : StrongLT a b) :

a ≤ b

theorem lt_of_strongLT {ι : Type u_1} {π : ι → Type u_4} [(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_4} [(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_4} [(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_4} [(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_4} [(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_4} [(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_4} [(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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :

x ≤ Function.update x i a ↔ x i ≤ a

@[simp]

theorem update_le_self_iff {ι : Type u_1} {π : ι → Type u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :

Function.update x i a ≤ x ↔ a ≤ x i

@[simp]

theorem lt_update_self_iff {ι : Type u_1} {π : ι → Type u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :

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

@[simp]

theorem update_lt_self_iff {ι : Type u_1} {π : ι → Type u_4} [DecidableEq ι] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :

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

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

SDiff ((i : ι) → π i)

Equations

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

theorem Pi.sdiff_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → SDiff (π i)] (x : (i : ι) → π i) (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 : (i : ι) → π i) (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 : α} :

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

@[simp]

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

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

`min`/`max` recursors #

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

p (min x y)

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

p (max x y)

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

p (min x y)

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

p (max x y)

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

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

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

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

Lifts of order instances #

@[reducible, inline]

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

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

Equations

Preorder.lift f = Preorder.mk ⋯ ⋯ ⋯

Instances For

@[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 note [reducible non-instances].

Equations

PartialOrder.lift f inj = PartialOrder.mk ⋯

Instances For

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

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

@[reducible, inline]

abbrev LinearOrder.lift {α : Type u_2} {β : Type u_3} [LinearOrder β] [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

LinearOrder.lift f inj hsup hinf = LinearOrder.mk ⋯ (fun (x y : α) => inferInstance) (fun (x y : α) => decidable_of_iff (f x = f y) ⋯) (fun (x y : α) => inferInstance) ⋯ ⋯ ⋯

Instances For

@[reducible, inline]

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

Transfer a LinearOrder on β to a LinearOrder on α using an injective function f : α → β. This version autogenerates min and max fields. See LinearOrder.lift for a version that takes [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

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

Instances For

@[reducible, inline]

abbrev LinearOrder.liftWithOrd {α : Type u_2} {β : Type u_3} [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

LinearOrder.liftWithOrd f inj hsup hinf compare_f = LinearOrder.mk ⋯ (fun (x y : α) => inferInstance) (fun (x y : α) => decidable_of_iff (f x = f y) ⋯) (fun (x y : α) => inferInstance) ⋯ ⋯ ⋯

Instances For

@[reducible, inline]

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

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

Equations

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

Instances For

Subtype of an order #

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

Equations

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

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

Equations

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

@[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 : Subtype p} {y : Subtype p} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

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

↑x < ↑y ↔ x < y

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

Preorder (Subtype p)

Equations

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

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

PartialOrder (Subtype p)

Equations

Subtype.partialOrder p = PartialOrder.lift (fun (a : Subtype p) => ↑a) ⋯

instance Subtype.decidableLE {α : Type u_2} [Preorder α] [h : DecidableRel fun (x1 x2 : α) => x1 ≤ x2] {p : α → Prop} :

DecidableRel fun (x1 x2 : Subtype p) => x1 ≤ x2

Equations

a.decidableLE b = h ↑a ↑b

instance Subtype.decidableLT {α : Type u_2} [Preorder α] [h : DecidableRel fun (x1 x2 : α) => x1 < x2] {p : α → Prop} :

DecidableRel fun (x1 x2 : Subtype p) => x1 < x2

Equations

a.decidableLT b = h ↑a ↑b

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

Subtype.instLinearOrder p = LinearOrder.lift (fun (a : Subtype p) => ↑a) ⋯ ⋯ ⋯

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_5) (β : Type u_6) [LE α] [LE β] :

LE (α × β)

Equations

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

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

Decidable (x ≤ y)

Equations

Prod.instDecidableLE α β x y = inferInstanceAs (Decidable (x.1 ≤ y.1 ∧ x.2 ≤ y.2))

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 β] {x₁ : α} {x₂ : α} {y₁ : β} {y₂ : β} :

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

@[simp]

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

x.swap ≤ y.swap ↔ x ≤ y

instance Prod.instPreorder (α : Type u_5) (β : Type u_6) [Preorder α] [Preorder β] :

Preorder (α × β)

Equations

Prod.instPreorder α β = Preorder.mk ⋯ ⋯ ⋯

@[simp]

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

x.swap < y.swap ↔ x < y

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

Equations

Prod.instPartialOrder α β = PartialOrder.mk ⋯

Additional order classes #

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

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

dense : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
An order is dense if there is an element between any pair of distinct elements.

Instances

theorem DenselyOrdered.dense {α : Type u_5} :

∀ {inst : LT α} [self : DenselyOrdered α] (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 exists_between {α : Type u_2} [LT α] [DenselyOrdered α] {a₁ : α} {a₂ : α} :

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

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

DenselyOrdered αᵒᵈ

Equations

⋯ = ⋯

@[simp]

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

DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

theorem Subsingleton.instDenselyOrdered {X : Type u_5} [Subsingleton X] [Preorder 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 (α × β)

Equations

⋯ = ⋯

instance instDenselyOrderedForall {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → Preorder (π i)] [∀ (i : ι), DenselyOrdered (π i)] :

DenselyOrdered ((i : ι) → π i)

Equations

⋯ = ⋯

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

a₁ ≤ a₂

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

a₁ = a₂

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

a₁ ≤ a₂

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

a₁ = a₂

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.

instance PUnit.instLinearOrder :

LinearOrder PUnit.{u_5 + 1}

Equations

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

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

max a b = PUnit.unit

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

min a b = PUnit.unit

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

a ≤ b

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

¬a < b

instance PUnit.instDenselyOrdered :

DenselyOrdered PUnit.{u_5 + 1}

Equations

PUnit.instDenselyOrdered = ⋯

instance Prop.le :

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

Equations

«Prop».le = { le := fun (x1 x2 : Prop) => x1 → x2 }

@[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 : α → α → Prop} {s : α → α → Prop} :

Subrelation r s ↔ r ≤ s

instance Prop.partialOrder :

PartialOrder Prop

Equations

«Prop».partialOrder = PartialOrder.mk «Prop».partialOrder.proof_2

Linear order from a total partial order #

def AsLinearOrder (α : Type u_5) :

Type u_5

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

Equations

AsLinearOrder α = α

Instances For

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

Inhabited (AsLinearOrder α)

Equations

instInhabitedAsLinearOrder = { default := default }

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

LinearOrder (AsLinearOrder α)

Equations

AsLinearOrder.linearOrder = LinearOrder.mk ⋯ (Classical.decRel fun (x1 x2 : AsLinearOrder α) => x1 ≤ x2) decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

theorem dite_nonneg {α : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [One α] {p : Prop} [Decidable p] {a : α} {b : α} [LT α] (ha : a < 1) (hb : b < 1) :

(if p then a else b) < 1