# 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} [] {a : α} {b : α} {c : α} :
b ca ba c
theorem lt_trans' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b < ca < ba < c
theorem lt_of_le_of_lt' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b ca < ba < c
theorem lt_of_lt_of_le' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b < ca ba < c
theorem ge_antisymm {α : Type u_2} [] {a : α} {b : α} :
a bb ab = a
theorem lt_of_le_of_ne' {α : Type u_2} [] {a : α} {b : α} :
a bb aa < b
theorem Ne.lt_of_le {α : Type u_2} [] {a : α} {b : α} :
a ba ba < b
theorem Ne.lt_of_le' {α : Type u_2} [] {a : α} {b : α} :
b aa ba < 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} [] {a : α} {b : α} {c : α} :
a bb ca c

Alias of le_trans.

The relation ≤ on a preorder is transitive.

theorem LE.le.trans' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b ca ba c

Alias of le_trans'.

theorem LE.le.trans_lt {α : Type u_1} [] {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} [] {a : α} {b : α} {c : α} :
b ca < ba < c

Alias of lt_of_le_of_lt'.

theorem LE.le.antisymm {α : Type u_1} [] {a : α} {b : α} :
a bb aa = b

Alias of le_antisymm.

theorem LE.le.antisymm' {α : Type u_2} [] {a : α} {b : α} :
a bb ab = a

Alias of ge_antisymm.

theorem LE.le.lt_of_ne {α : Type u_1} [] {a : α} {b : α} :
a ba ba < b

Alias of lt_of_le_of_ne.

theorem LE.le.lt_of_ne' {α : Type u_2} [] {a : α} {b : α} :
a bb aa < b

Alias of lt_of_le_of_ne'.

theorem LE.le.lt_of_not_le {α : Type u_1} [] {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} [] {a : α} {b : α} :
a ba < b a = b

Alias of lt_or_eq_of_le.

theorem LE.le.lt_or_eq_dec {α : Type u_1} [] {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} [] {a : α} {b : α} (hab : a < b) :
a b

Alias of le_of_lt.

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

Alias of lt_trans.

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

Alias of lt_trans'.

theorem LT.lt.trans_le {α : Type u_1} [] {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} [] {a : α} {b : α} {c : α} :
b < ca ba < c

Alias of lt_of_lt_of_le'.

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

Alias of ne_of_lt.

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

Alias of lt_asymm.

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

Alias of lt_asymm.

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

Alias of le_of_eq.

@[simp]
theorem lt_self_iff_false {α : Type u_2} [] (x : α) :
x < x False
theorem le_of_le_of_eq' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b ca = ba c
theorem le_of_eq_of_le' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b = ca ba c
theorem lt_of_lt_of_eq' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b < ca = ba < c
theorem lt_of_eq_of_lt' {α : Type u_2} [] {a : α} {b : α} {c : α} :
b = ca < ba < 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} [] {a : α} {b : α} {c : α} :
b ca = ba 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} [] {a : α} {b : α} {c : α} :
b < ca = ba < 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} [] {a : α} {b : α} {c : α} :
b = ca ba 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} [] {a : α} {b : α} {c : α} :
b = ca < ba < c

Alias of lt_of_eq_of_lt'.

theorem Eq.ge {α : Type u_2} [] {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} [] {x : α} {y : α} (h : x = y) :
¬x < y
theorem Eq.not_gt {α : Type u_2} [] {x : α} {y : α} (h : x = y) :
¬y < x
@[simp]
theorem le_of_subsingleton {α : Type u_2} [] {a : α} {b : α} [] :
a b
theorem not_lt_of_subsingleton {α : Type u_2} [] {a : α} {b : α} [] :
¬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} [] {a : α} {b : α} (h : a b) :
a < b a b
theorem LE.le.gt_iff_ne {α : Type u_2} [] {a : α} {b : α} (h : a b) :
a < b b a
theorem LE.le.not_lt_iff_eq {α : Type u_2} [] {a : α} {b : α} (h : a b) :
¬a < b a = b
theorem LE.le.not_gt_iff_eq {α : Type u_2} [] {a : α} {b : α} (h : a b) :
¬a < b b = a
theorem LE.le.le_iff_eq {α : Type u_2} [] {a : α} {b : α} (h : a b) :
b a b = a
theorem LE.le.ge_iff_eq {α : Type u_2} [] {a : α} {b : α} (h : a b) :
b a a = b
theorem LE.le.lt_or_le {α : Type u_2} [] {a : α} {b : α} (h : a b) (c : α) :
a < c c b
theorem LE.le.le_or_lt {α : Type u_2} [] {a : α} {b : α} (h : a b) (c : α) :
a c c < b
theorem LE.le.le_or_le {α : Type u_2} [] {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} [] {x : α} :
x < xFalse
theorem LT.lt.ne' {α : Type u_2} [] {x : α} {y : α} (h : x < y) :
y x
theorem LT.lt.lt_or_lt {α : Type u_2} [] {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} [] {a : α} {b : α} (h : a = b) :
a b
theorem ne_of_not_le {α : Type u_2} [] {a : α} {b : α} (h : ¬a b) :
a b
theorem Decidable.le_iff_eq_or_lt {α : Type u_2} [] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 x2] :
a b a = b a < b
theorem le_iff_eq_or_lt {α : Type u_2} [] {a : α} {b : α} :
a b a = b a < b
theorem lt_iff_le_and_ne {α : Type u_2} [] {a : α} {b : α} :
a < b a b a b
theorem eq_iff_not_lt_of_le {α : Type u_2} [] {a : α} {b : α} (hab : a b) :
a = b ¬a < b
theorem LE.le.eq_iff_not_lt {α : Type u_2} [] {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} [] {a : α} {b : α} [DecidableRel fun (x1 x2 : α) => x1 x2] :
a = b a b ¬a < b
theorem eq_iff_le_not_lt {α : Type u_2} [] {a : α} {b : α} :
a = b a b ¬a < b
theorem eq_or_lt_of_le {α : Type u_2} [] {a : α} {b : α} (h : a b) :
a = b a < b
theorem eq_or_gt_of_le {α : Type u_2} [] {a : α} {b : α} (h : a b) :
b = a a < b
theorem gt_or_eq_of_le {α : Type u_2} [] {a : α} {b : α} (h : a b) :
a < b b = a
theorem LE.le.eq_or_lt_dec {α : Type u_1} [] {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} [] {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} [] {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} [] {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} [] {a : α} {b : α} (hab : a b) (hba : ¬a < b) :
a = b
theorem eq_of_ge_of_not_gt {α : Type u_2} [] {a : α} {b : α} (hab : a b) (hba : ¬a < b) :
b = a
theorem LE.le.eq_of_not_lt {α : Type u_2} [] {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} [] {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} [] {a : α} {b : α} (h : a b) :
a b a < b
theorem Ne.not_le_or_not_le {α : Type u_2} [] {a : α} {b : α} (h : a b) :
¬a b ¬b a
theorem Decidable.ne_iff_lt_iff_le {α : Type u_2} [] {a : α} {b : α} [] :
(a b a < b) a b
@[simp]
theorem ne_iff_lt_iff_le {α : Type u_2} [] {a : α} {b : α} :
(a b a < b) a b
theorem min_def' {α : Type u_2} [] (a : α) (b : α) :
min a b = if b a then b else a
theorem max_def' {α : Type u_2} [] (a : α) (b : α) :
max a b = if b a then a else b
theorem lt_of_not_le {α : Type u_2} [] {a : α} {b : α} (h : ¬b a) :
a < b
theorem lt_iff_not_le {α : Type u_2} [] {x : α} {y : α} :
x < y ¬y x
theorem Ne.lt_or_lt {α : Type u_2} [] {x : α} {y : α} (h : x y) :
x < y y < x
@[simp]
theorem lt_or_lt_iff_ne {α : Type u_2} [] {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} [] {a : α} {b : α} :
¬a < b a = b b < a
theorem exists_ge_of_linear {α : Type u_2} [] (a : α) (b : α) :
∃ (c : α), a c b c
theorem exists_forall_ge_and {α : Type u_2} [] {p : αProp} {q : αProp} :
(∃ (i : α), ∀ (j : α), j ip j)(∃ (i : α), ∀ (j : α), j iq j)∃ (i : α), ∀ (j : α), j ip j q j
theorem lt_imp_lt_of_le_imp_le {α : Type u_2} {β : Type u_5} [] [] {a : α} {b : α} {c : β} {d : β} (H : a bc d) (h : d < c) :
b < a
theorem le_imp_le_iff_lt_imp_lt {α : Type u_2} {β : Type u_5} [] [] {a : α} {b : α} {c : β} {d : β} :
a bc d d < cb < a
theorem lt_iff_lt_of_le_iff_le' {α : Type u_2} {β : Type u_5} [] [] {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} [] [] {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} [] [] {a : α} {b : α} {c : β} {d : β} :
(a b c d) (b < a d < c)
theorem eq_of_forall_le_iff {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), c a c b) :
a = b
theorem le_of_forall_le {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), c ac b) :
a b
theorem le_of_forall_le' {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), a cb c) :
b a
theorem le_of_forall_lt {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), c < ac < b) :
a b
theorem forall_lt_iff_le {α : Type u_2} [] {a : α} {b : α} :
(∀ ⦃c : α⦄, c < ac < b) a b
theorem le_of_forall_lt' {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), a < cb < c) :
b a
theorem forall_lt_iff_le' {α : Type u_2} [] {a : α} {b : α} :
(∀ ⦃c : α⦄, a < cb < c) b a
theorem eq_of_forall_ge_iff {α : Type u_2} [] {a : α} {b : α} (H : ∀ (c : α), a c b c) :
a = b
theorem eq_of_forall_lt_iff {α : Type u_2} [] {a : α} {b : α} (h : ∀ (c : α), c < a c < b) :
a = b
theorem eq_of_forall_gt_iff {α : Type u_2} [] {a : α} {b : α} (h : ∀ (c : α), a < c b < c) :
a = b
theorem rel_imp_eq_of_rel_imp_le {α : Type u_2} {β : Type u_3} [] (r : ααProp) [IsSymm α r] {f : αβ} (h : ∀ (a b : α), r a bf a f b) {a : α} {b : α} :
r a bf 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 : α} [] (hca : c a) (hbd : b d) :
a bc d

monotonicity of ≤ with respect to →

theorem commutative_of_le {α : Type u_2} {β : Type u_3} [] {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} [] {f : ααα} (comm : ) (assoc : ∀ (a b c : α), f (f a b) c f a (f b c)) :

To prove associativity of a commutative binary operation ○, we only to check (a ○ b) ○ c ≤ a ○ (b ○ c) for all a, b, c.

theorem Preorder.toLE_injective_iff {α : Type u_2} {a₁ : } {a₂ : } :
a₁ = a₂ Preorder.toLE = Preorder.toLE
theorem Preorder.toLE_injective {α : Type u_2} :
theorem PartialOrder.toPreorder_injective_iff {α : Type u_2} {a₁ : } {a₂ : } :
a₁ = a₂ PartialOrder.toPreorder = PartialOrder.toPreorder
theorem LinearOrder.toPartialOrder_injective_iff {α : Type u_2} {a₁ : } {a₂ : } :
a₁ = a₂ LinearOrder.toPartialOrder = LinearOrder.toPartialOrder
theorem Preorder.ext {α : Type u_2} {A : } {B : } (H : ∀ (x y : α), x y x y) :
A = B
theorem PartialOrder.ext {α : Type u_2} {A : } {B : } (H : ∀ (x y : α), x y x y) :
A = B
theorem LinearOrder.ext {α : Type u_2} {A : } {B : } (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
Instances For

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
Instances For
instance Order.Preimage.decidable {α : Type u_2} {β : Type u_3} (f : αβ) (s : ββProp) [H : ] :

The preimage of a decidable order is decidable.

Equations
• = H (f x✝) (f x)
@[simp]
theorem ltByCases_lt {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : x < y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
ltByCases x y h₁ h₂ h₃ = h₁ h
@[simp]
theorem ltByCases_gt {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : y < x) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
ltByCases x y h₁ h₂ h₃ = h₃ h
@[simp]
theorem ltByCases_eq {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : x = y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} :
ltByCases x y h₁ h₂ h₃ = h₂ h
theorem ltByCases_not_lt {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : ¬x < y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : optParam (¬y < xx = y) ) :
ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂
theorem ltByCases_not_gt {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : ¬y < x) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : optParam (¬x < yx = y) ) :
ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂
theorem ltByCases_ne {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} (h : x y) {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : optParam (¬x < yy < x) ) :
ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃
theorem ltByCases_comm {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (p : optParam (y = xx = 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} [] {x : α} {y : α} {x' : α} {y' : α} (ltc : x < y x' < y') (gtc : y < x y' < x') :
x = y x' = y'
theorem ltByCases_rec {α : Type u_2} [] {P : Sort u_5} {x : α} {y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} (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} [] {P : Sort u_5} {x : α} {y : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} {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} [] {P : Sort u_5} {x : α} {y : α} {x' : α} {y' : α} {h₁ : x < yP} {h₂ : x = yP} {h₃ : y < xP} {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} [] {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
Instances For
@[simp]
theorem ltTrichotomy_lt {α : Type u_2} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {P : Sort u_5} {x : α} {y : α} {p : P} :
ltTrichotomy x y p p p = p
theorem ltTrichotomy_eq_iff {α : Type u_2} [] {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} [] {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

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

Equations
Instances For
instance OrderDual.instNonempty (α : Type u_5) [h : ] :
Equations
• = h
instance OrderDual.instSubsingleton (α : Type u_5) [h : ] :
Equations
• = h
instance OrderDual.instLE (α : Type u_5) [LE α] :
Equations
• = { le := fun (x y : α) => y x }
instance OrderDual.instLT (α : Type u_5) [LT α] :
Equations
• = { lt := fun (x y : α) => y < x }
instance OrderDual.instPreorder (α : Type u_5) [] :
Equations
instance OrderDual.instPartialOrder (α : Type u_5) [] :
Equations
instance OrderDual.instLinearOrder (α : Type u_5) [] :
Equations
• = LinearOrder.mk inferInstance decidableEqOfDecidableLE inferInstance
instance OrderDual.instInhabited {α : Type u_2} [] :
Equations
• OrderDual.instInhabited = x
theorem OrderDual.Preorder.dual_dual (α : Type u_5) [H : ] :

### HasCompl#

instance Prop.hasCompl :
Equations
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] :
Equations
• =

### 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
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 =
@[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₂ v₁ 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₁ u₂
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
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} [] (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} [] (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} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} :
x x i a ∀ (j : ι), j ix j y j
theorem update_le_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} :
y a y i ∀ (j : ι), j ix j y j
theorem update_le_update_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {y : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :
a b ∀ (j : ι), j ix j y j
@[simp]
theorem update_le_update_iff' {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :
a b
@[simp]
theorem update_lt_update_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} {b : π i} :
< a < b
@[simp]
theorem le_update_self_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
x x i a
@[simp]
theorem update_le_self_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
x a x i
@[simp]
theorem lt_update_self_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
x < x i < a
@[simp]
theorem update_lt_self_iff {ι : Type u_1} {π : ιType u_4} [] [(i : ι) → Preorder (π i)] {x : (i : ι) → π i} {i : ι} {a : π i} :
< 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} [] [] {a : α} {b : α} :
a b
@[simp]
theorem Function.const_lt_const {α : Type u_2} {β : Type u_3} [] [] {a : α} {b : α} :
< a < b

### min/max recursors #

theorem min_rec {α : Type u_2} [] {p : αProp} {x : α} {y : α} (hx : x yp x) (hy : y xp y) :
p (min x y)
theorem max_rec {α : Type u_2} [] {p : αProp} {x : α} {y : α} (hx : y xp x) (hy : x yp y) :
p (max x y)
theorem min_rec' {α : Type u_2} [] {x : α} {y : α} (p : αProp) (hx : p x) (hy : p y) :
p (min x y)
theorem max_rec' {α : Type u_2} [] {x : α} {y : α} (p : αProp) (hx : p x) (hy : p y) :
p (max x y)
theorem min_def_lt {α : Type u_2} [] (x : α) (y : α) :
min x y = if x < y then x else y
theorem max_def_lt {α : Type u_2} [] (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} [] (f : αβ) :

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

Equations
Instances For
@[reducible, inline]
abbrev PartialOrder.lift {α : Type u_2} {β : Type u_3} [] (f : αβ) (inj : ) :

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

Equations
Instances For
theorem compare_of_injective_eq_compareOfLessAndEq {α : Type u_2} {β : Type u_3} (a : α) (b : α) [] [] (f : αβ) (inj : ) [Decidable (a < b)] :
compare (f a) (f b) =
@[reducible, inline]
abbrev LinearOrder.lift {α : Type u_2} {β : Type u_3} [] [Sup α] [Inf α] (f : αβ) (inj : ) (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
Instances For
@[reducible, inline]
abbrev LinearOrder.lift' {α : Type u_2} {β : Type u_3} [] (f : αβ) (inj : ) :

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
Instances For
@[reducible, inline]
abbrev LinearOrder.liftWithOrd {α : Type u_2} {β : Type u_3} [] [Sup α] [Inf α] [Ord α] (f : αβ) (inj : ) (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
Instances For
@[reducible, inline]
abbrev LinearOrder.liftWithOrd' {α : Type u_2} {β : Type u_3} [] [Ord α] (f : αβ) (inj : ) (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
Instances For

### Subtype of an order #

instance Subtype.le {α : Type u_2} [LE α] {p : αProp} :
Equations
• Subtype.le = { le := fun (x y : ) => x y }
instance Subtype.lt {α : Type u_2} [LT α] {p : αProp} :
Equations
• Subtype.lt = { lt := fun (x y : ) => 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 : } {y : } :
x y x y
@[simp]
theorem Subtype.coe_lt_coe {α : Type u_2} [LT α] {p : αProp} {x : } {y : } :
x < y x < y
instance Subtype.preorder {α : Type u_2} [] (p : αProp) :
Equations
instance Subtype.partialOrder {α : Type u_2} [] (p : αProp) :
Equations
instance Subtype.decidableLE {α : Type u_2} [] [h : DecidableRel fun (x1 x2 : α) => x1 x2] {p : αProp} :
DecidableRel fun (x1 x2 : ) => x1 x2
Equations
• a.decidableLE b = h a b
instance Subtype.decidableLT {α : Type u_2} [] [h : DecidableRel fun (x1 x2 : α) => x1 < x2] {p : αProp} :
DecidableRel fun (x1 x2 : ) => x1 < x2
Equations
• a.decidableLT b = h a b
instance Subtype.instLinearOrder {α : Type u_2} [] (p : αProp) :

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

### 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
• = { 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)] :
Equations
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 (α × β)
Equations
@[simp]
theorem Prod.swap_lt_swap {α : Type u_2} {β : Type u_3} [] [] {x : α × β} {y : α × β} :
x.swap < y.swap x < y
theorem Prod.mk_le_mk_iff_left {α : Type u_2} {β : Type u_3} [] [] {a₁ : α} {a₂ : α} {b : β} :
(a₁, b) (a₂, b) a₁ a₂
theorem Prod.mk_le_mk_iff_right {α : Type u_2} {β : Type u_3} [] [] {a : α} {b₁ : β} {b₂ : β} :
(a, b₁) (a, b₂) b₁ b₂
theorem Prod.mk_lt_mk_iff_left {α : Type u_2} {β : Type u_3} [] [] {a₁ : α} {a₂ : α} {b : β} :
(a₁, b) < (a₂, b) a₁ < a₂
theorem Prod.mk_lt_mk_iff_right {α : Type u_2} {β : Type u_3} [] [] {a : α} {b₁ : β} {b₂ : β} :
(a, b₁) < (a, b₂) b₁ < b₂
theorem Prod.lt_iff {α : Type u_2} {β : Type u_3} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {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} [] [] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} (h₁ : a₁ a₂) (h₂ : b₁ < b₂) :
(a₁, b₁) < (a₂, b₂)
instance Prod.instPartialOrder (α : Type u_5) (β : Type u_6) [] [] :

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

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} [LT α] [self : ] (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 α] [] {a₁ : α} {a₂ : α} :
a₁ < a₂∃ (a : α), a₁ < a a < a₂
instance OrderDual.denselyOrdered (α : Type u_5) [LT α] [h : ] :
Equations
• =
@[simp]
theorem denselyOrdered_orderDual {α : Type u_2} [LT α] :
theorem Subsingleton.instDenselyOrdered {X : Type u_5} [] [] :

Any ordered subsingleton is densely ordered. Not an instance to avoid a heavy subsingleton typeclass search.

instance instDenselyOrderedProd {α : Type u_2} {β : Type u_3} [] [] [] [] :
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} [] [] {a₁ : α} {a₂ : α} (h : ∀ (a : α), a₂ < aa₁ a) :
a₁ a₂
theorem eq_of_le_of_forall_le_of_dense {α : Type u_2} [] [] {a₁ : α} {a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a : α), a₂ < aa₁ a) :
a₁ = a₂
theorem le_of_forall_ge_of_dense {α : Type u_2} [] [] {a₁ : α} {a₂ : α} (h : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
a₁ a₂
theorem eq_of_le_of_forall_ge_of_dense {α : Type u_2} [] [] {a₁ : α} {a₂ : α} (h₁ : a₂ a₁) (h₂ : ∀ (a₃ : α), a₃ < a₁a₃ a₂) :
a₁ = a₂
theorem dense_or_discrete {α : Type u_2} [] (a₁ : α) (a₂ : α) :
(∃ (a : α), a₁ < a a < a₂) (∀ (a : α), a₁ < aa₂ a) ∀ (a : α), a < a₂a a₁
theorem eq_or_eq_or_eq_of_forall_not_lt_lt {α : Type u_2} [] (h : ∀ ⦃x y z : α⦄, x < yy < zFalse) (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.

Equations
• One or more equations did not get rendered due to their size.
Equations
instance Prop.le :

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

Equations
@[simp]
theorem le_Prop_eq :
(fun (x1 x2 : Prop) => x1 x2) = fun (x1 x2 : Prop) => x1x2
theorem subrelation_iff_le {α : Type u_2} {r : ααProp} {s : ααProp} :
r s

### 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
Instances For
instance instInhabitedAsLinearOrder {α : Type u_2} [] :
Equations
• instInhabitedAsLinearOrder = { default := default }
noncomputable instance AsLinearOrder.linearOrder {α : Type u_2} [] [IsTotal α fun (x1 x2 : α) => x1 x2] :
Equations
theorem dite_nonneg {α : Type u_2} [Zero α] {p : Prop} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {a : α} {b : α} [LT α] (ha : a < 1) (hb : b < 1) :
(if p then a else b) < 1