mathlib documentation

core.init.algebra.order

@[instance]

def preorder.to_has_lt (α : Type u) [s : preorder α] :

@[class]

structure preorder (α : Type u) :

Type u

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"

A preorder is a reflexive, transitive relation ≤ with a < b defined in the obvious way.

Instances

@[instance]

def preorder.to_has_le (α : Type u) [s : preorder α] :

@[class]

structure partial_order (α : Type u) :

Type u

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b

A partial order is a reflexive, transitive, antisymmetric relation ≤.

Instances

@[instance]

def partial_order.to_preorder (α : Type u) [s : partial_order α] :

@[class]

structure linear_order (α : Type u) :

Type u

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a

A linear order is reflexive, transitive, antisymmetric and total relation ≤.

Instances

@[instance]

def linear_order.to_partial_order (α : Type u) [s : linear_order α] :

partial_order α

theorem le_refl {α : Type u} [preorder α] (a : α) :

a ≤ a

The relation ≤ on a preorder is reflexive.

theorem le_trans {α : Type u} [preorder α] {a b c : α} (a_1 : a ≤ b) (a_2 : b ≤ c) :

a ≤ c

The relation ≤ on a preorder is transitive.

theorem lt_iff_le_not_le {α : Type u} [preorder α] {a b : α} :

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

theorem lt_of_le_not_le {α : Type u} [preorder α] {a b : α} (a_1 : a ≤ b) (a_2 : ¬b ≤ a) :

a < b

theorem le_not_le_of_lt {α : Type u} [preorder α] {a b : α} (a_1 : a < b) :

a ≤ b ∧ ¬b ≤ a

theorem le_antisymm {α : Type u} [partial_order α] {a b : α} (a_1 : a ≤ b) (a_2 : b ≤ a) :

a = b

theorem le_of_eq {α : Type u} [preorder α] {a b : α} (a_1 : a = b) :

a ≤ b

theorem le_antisymm_iff {α : Type u} [partial_order α] {a b : α} :

a = b ↔ a ≤ b ∧ b ≤ a

theorem ge_trans {α : Type u} [preorder α] {a b c : α} (a_1 : a ≥ b) (a_2 : b ≥ c) :

a ≥ c

theorem le_total {α : Type u} [linear_order α] (a b : α) :

a ≤ b ∨ b ≤ a

theorem le_of_not_ge {α : Type u} [linear_order α] {a b : α} (a_1 : ¬a ≥ b) :

a ≤ b

theorem le_of_not_le {α : Type u} [linear_order α] {a b : α} (a_1 : ¬a ≤ b) :

b ≤ a

theorem lt_irrefl {α : Type u} [preorder α] (a : α) :

¬a < a

theorem gt_irrefl {α : Type u} [preorder α] (a : α) :

¬a > a

theorem lt_trans {α : Type u} [preorder α] {a b c : α} (a_1 : a < b) (a_2 : b < c) :

a < c

def lt.trans {α : Type u_1} [preorder α] {a b c : α} (a_1 : a < b) (a_2 : b < c) :

a < c

theorem gt_trans {α : Type u} [preorder α] {a b c : α} (a_1 : a > b) (a_2 : b > c) :

a > c

def gt.trans {α : Type u_1} [preorder α] {a b c : α} (a_1 : a > b) (a_2 : b > c) :

a > c

theorem ne_of_lt {α : Type u} [preorder α] {a b : α} (h : a < b) :

a ≠ b

theorem ne_of_gt {α : Type u} [preorder α] {a b : α} (h : a > b) :

a ≠ b

theorem lt_asymm {α : Type u} [preorder α] {a b : α} (h : a < b) :

¬b < a

theorem not_lt_of_gt {α : Type u} [linear_order α] {a b : α} (h : a > b) :

¬a < b

theorem le_of_lt {α : Type u} [preorder α] {a b : α} (a_1 : a < b) :

a ≤ b

theorem lt_of_lt_of_le {α : Type u} [preorder α] {a b c : α} (a_1 : a < b) (a_2 : b ≤ c) :

a < c

theorem lt_of_le_of_lt {α : Type u} [preorder α] {a b c : α} (a_1 : a ≤ b) (a_2 : b < c) :

a < c

theorem gt_of_gt_of_ge {α : Type u} [preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) :

a > c

theorem gt_of_ge_of_gt {α : Type u} [preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) :

a > c

theorem not_le_of_gt {α : Type u} [preorder α] {a b : α} (h : a > b) :

theorem not_lt_of_ge {α : Type u} [preorder α] {a b : α} (h : a ≥ b) :

¬a < b

theorem lt_or_eq_of_le {α : Type u} [partial_order α] {a b : α} (a_1 : a ≤ b) :

a < b ∨ a = b

theorem le_of_lt_or_eq {α : Type u} [preorder α] {a b : α} (a_1 : a < b ∨ a = b) :

a ≤ b

theorem le_iff_lt_or_eq {α : Type u} [partial_order α] {a b : α} :

a ≤ b ↔ a < b ∨ a = b

theorem lt_of_le_of_ne {α : Type u} [partial_order α] {a b : α} (a_1 : a ≤ b) (a_2 : a ≠ b) :

a < b

theorem lt_trichotomy {α : Type u} [linear_order α] (a b : α) :

a < b ∨ a = b ∨ b < a

theorem le_of_not_gt {α : Type u} [linear_order α] {a b : α} (h : ¬a > b) :

a ≤ b

theorem lt_of_not_ge {α : Type u} [linear_order α] {a b : α} (h : ¬a ≥ b) :

a < b

theorem lt_or_ge {α : Type u} [linear_order α] (a b : α) :

a < b ∨ a ≥ b

theorem le_or_gt {α : Type u} [linear_order α] (a b : α) :

a ≤ b ∨ a > b

theorem lt_or_gt_of_ne {α : Type u} [linear_order α] {a b : α} (h : a ≠ b) :

a < b ∨ a > b

theorem le_of_eq_or_lt {α : Type u} [preorder α] {a b : α} (h : a = b ∨ a < b) :

a ≤ b

theorem ne_iff_lt_or_gt {α : Type u} [linear_order α] {a b : α} :

a ≠ b ↔ a < b ∨ a > b

theorem lt_iff_not_ge {α : Type u} [linear_order α] (x y : α) :

x < y ↔ ¬x ≥ y

@[simp]

theorem not_lt {α : Type u} [linear_order α] {a b : α} :

¬a < b ↔ b ≤ a

@[simp]

theorem not_le {α : Type u} [linear_order α] {a b : α} :

¬a ≤ b ↔ b < a

@[instance]

def decidable_lt_of_decidable_le {α : Type u} [preorder α] [decidable_rel has_le.le] :

decidable_rel has_lt.lt

Equations

decidable_lt_of_decidable_le a b = dite (a ≤ b) (λ (hab : a ≤ b), dite (b ≤ a) (λ (hba : b ≤ a), is_false _) (λ (hba : ¬b ≤ a), is_true _)) (λ (hab : ¬a ≤ b), is_false _)

@[instance]

def decidable_eq_of_decidable_le {α : Type u} [partial_order α] [decidable_rel has_le.le] :

decidable_eq α

Equations

decidable_eq_of_decidable_le a b = dite (a ≤ b) (λ (hab : a ≤ b), dite (b ≤ a) (λ (hba : b ≤ a), is_true _) (λ (hba : ¬b ≤ a), is_false _)) (λ (hab : ¬a ≤ b), is_false _)

@[class]

structure decidable_linear_order (α : Type u) :

Type u

le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
decidable_le : decidable_rel has_le.le
decidable_eq : decidable_eq α
decidable_lt : decidable_rel has_lt.lt

Instances

@[instance]

def decidable_linear_order.to_linear_order (α : Type u) [s : decidable_linear_order α] :

linear_order α

@[instance]

def has_lt.lt.decidable {α : Type u} [decidable_linear_order α] (a b : α) :

decidable (a < b)

Equations

has_lt.lt.decidable a b = decidable_linear_order.decidable_lt a b

@[instance]

def has_le.le.decidable {α : Type u} [decidable_linear_order α] (a b : α) :

decidable (a ≤ b)

Equations

has_le.le.decidable a b = decidable_linear_order.decidable_le a b

@[instance]

def eq.decidable {α : Type u} [decidable_linear_order α] (a b : α) :

decidable (a = b)

Equations

eq.decidable a b = decidable_linear_order.decidable_eq a b

theorem eq_or_lt_of_not_lt {α : Type u} [decidable_linear_order α] {a b : α} (h : ¬a < b) :

a = b ∨ b < a

@[instance]

def has_le.le.is_total_preorder {α : Type u} [decidable_linear_order α] :

is_total_preorder α has_le.le

@[instance]

def is_strict_weak_order_of_decidable_linear_order {α : Type u} [decidable_linear_order α] :

is_strict_weak_order α has_lt.lt

@[instance]

def is_strict_total_order_of_decidable_linear_order {α : Type u} [decidable_linear_order α] :

is_strict_total_order α has_lt.lt

theorem decidable.lt_or_eq_of_le {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} (hab : a ≤ b) :

a < b ∨ a = b

theorem decidable.eq_or_lt_of_le {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} (hab : a ≤ b) :

a = b ∨ a < b

theorem decidable.le_iff_lt_or_eq {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :

a ≤ b ↔ a < b ∨ a = b

theorem decidable.le_of_not_lt {α : Type u} [decidable_linear_order α] {a b : α} (h : ¬b < a) :

a ≤ b

theorem decidable.not_lt {α : Type u} [decidable_linear_order α] {a b : α} :

¬a < b ↔ b ≤ a

theorem decidable.lt_or_le {α : Type u} [decidable_linear_order α] (a b : α) :

a < b ∨ b ≤ a

theorem decidable.le_or_lt {α : Type u} [decidable_linear_order α] (a b : α) :

a ≤ b ∨ b < a

theorem decidable.lt_trichotomy {α : Type u} [decidable_linear_order α] (a b : α) :

a < b ∨ a = b ∨ b < a

theorem decidable.lt_or_gt_of_ne {α : Type u} [decidable_linear_order α] {a b : α} (h : a ≠ b) :

a < b ∨ b < a

def decidable.lt_by_cases {α : Type u} [decidable_linear_order α] (x y : α) {P : Sort u_1} (h₁ : x < y → P) (h₂ : x = y → P) (h₃ : y < x → P) :

P

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

Equations

decidable.lt_by_cases x y h₁ h₂ h₃ = dite (x < y) (λ (h : x < y), h₁ h) (λ (h : ¬x < y), dite (y < x) (λ (h' : y < x), h₃ h') (λ (h' : ¬y < x), h₂ _))

theorem decidable.ne_iff_lt_or_gt {α : Type u} [decidable_linear_order α] {a b : α} :

a ≠ b ↔ a < b ∨ b < a

theorem decidable.le_imp_le_of_lt_imp_lt {α : Type u} {β : Type u_1} [preorder α] [decidable_linear_order β] {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) :

c ≤ d