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

• Sup: type class for the ⊔ notation
• Inf: type class for the ⊓ notation
• HasCompl: type class for the ᶜ notation
• 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 : α} (hab : a ≤ b) (hbc : b = c) : a ≤ c

theorem le_of_eq_of_le {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b ≤ c) : a ≤ c

theorem lt_of_lt_of_eq {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a < b) (hbc : b = c) : a < c

theorem lt_of_eq_of_lt {α : Type u} [Preorder α] {a : α} {b : α} {c : α} (hab : a = b) (hbc : b < c) : a < c

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

@[simp]

theorem ge_iff_le {α : Type u} [LE α] {a : α} {b : α} : a ≥ b ↔ b ≤ a

@[simp]

theorem gt_iff_lt {α : Type u} [LT α] {a : α} {b : α} : a > b ↔ b < a

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

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

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

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

Equations

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

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

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

Equations

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

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

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

• αᵒᵈ = α

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 "ᵒᵈ")

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 α] : LE αᵒᵈ

Equations

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

instance OrderDual.instLTOrderDual (α : Type u_3) [LT α] : 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

class HasCompl (α : Type u_3) : Type u_3

• compl : α → α

  Set / lattice complement

Set / lattice complement

def «term_ᶜ» : Lean.TrailingParserDescr

Set / lattice complement

Equations

• «term_ᶜ» = Lean.ParserDescr.trailingNode `term_ᶜ 1024 1024 (Lean.ParserDescr.symbol "ᶜ")

instance Prop.hasCompl : HasCompl Prop

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 => (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 : ι) : ((i : ι) → α i)ᶜ Pi.hasCompl x i = (x i)ᶜ

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

Equations

• @IsIrrefl.compl = @IsIrrefl.compl.proof_1

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

Equations

• @IsRefl.compl = @IsRefl.compl.proof_1

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 : ι), 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) : Prop

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

Equations

• StrongLT a b = ∀ (i : ι), a i < b i

theorem le_of_strongLT {ι : Type u_1} {π : ι → Type u_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) : StrongLT a 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) : StrongLT a 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) : StrongLT a 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) : StrongLT a 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 => 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 : ι) : (((i : ι) → α i) \ Pi.sdiff) 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

Sup and Inf

theorem Sup.ext {α : Type u} (x : Sup α) (y : Sup α) (sup : Sup.sup = Sup.sup) : x = y

theorem Sup.ext_iff {α : Type u} (x : Sup α) (y : Sup α) : x = y ↔ Sup.sup = Sup.sup

class Sup (α : Type u) : Type u

• sup : α → α → α

  Least upper bound (\lub notation)

Typeclass for the ⊔ (\lub) notation

theorem Inf.ext {α : Type u} (x : Inf α) (y : Inf α) (inf : Inf.inf = Inf.inf) : x = y

theorem Inf.ext_iff {α : Type u} (x : Inf α) (y : Inf α) : x = y ↔ Inf.inf = Inf.inf

class Inf (α : Type u) : Type u

• inf : α → α → α

  Greatest lower bound (\glb notation)

Typeclass for the ⊓ (\glb) notation

def «term_⊔_» : Lean.TrailingParserDescr

Least upper bound (\lub notation)

Equations

• «term_⊔_» = Lean.ParserDescr.trailingNode `term_⊔_ 68 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊔ ") (Lean.ParserDescr.cat `term 69))

def «term_⊓_» : Lean.TrailingParserDescr

Greatest lower bound (\glb notation)

Equations

• «term_⊓_» = Lean.ParserDescr.trailingNode `term_⊓_ 69 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊓ ") (Lean.ParserDescr.cat `term 70))

Lifts of order instances

@[reducible]

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

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)

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

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

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.

@[reducible]

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

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

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

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.

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

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

Equations

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

Subtype of an order

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

Equations

• Subtype.le = { le := fun x y => ↑x ≤ ↑y }

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

Equations

• Subtype.lt = { lt := fun x y => ↑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 => ↑a

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

Equations

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

instance Subtype.decidableLE {α : Type u} [Preorder α] [h : DecidableRel fun x x_1 => x ≤ x_1] {p : α → Prop} : DecidableRel fun x x_1 => 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 => 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.fst ≤ q.fst ∧ p.snd ≤ q.snd }

instance Prod.instDecidableLE (α : Type u) (β : Type v) [LE α] [LE β] (x : α × β) (y : α × β) [Decidable (x.fst ≤ y.fst)] [Decidable (x.snd ≤ y.snd)] : 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.fst ≤ y.fst ∧ x.snd ≤ y.snd

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

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

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

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

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

• OrderDual.denselyOrdered = OrderDual.denselyOrdered.proof_1

@[simp]

theorem denselyOrdered_orderDual {α : Type u} [LT α] : DenselyOrdered αᵒᵈ ↔ DenselyOrdered α

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

Equations

• @instDenselyOrderedProdToLTInstPreorderProd = @instDenselyOrderedProdToLTInstPreorderProd.proof_1

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

Equations

• @instDenselyOrderedForAllToLTPreorder = @instDenselyOrderedForAllToLTPreorder.proof_1

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 = PUnit.instDenselyOrderedPUnitToLTToPreorderToPartialOrderLinearOrder.proof_1

instance Prop.le : LE Prop

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

Equations

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

@[simp]

theorem le_Prop_eq : (fun x x_1 => x ≤ x_1) = fun x x_1 => 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 u

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

Equations

• AsLinearOrder α = α

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