mathlib documentation

core / init.algebra.order

Definition of preorder and lemmas about types with a preorder #

source
@[instance]
def preorder.to_has_lt (α : Type u) [self : preorder α] :
has_lt α
source
@[class]
structure preorder (α : Type u) :
Type u
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • 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
source
@[instance]
def preorder.to_has_le (α : Type u) [self : preorder α] :
has_le α
source
@[simp]
theorem le_refl {α : Type u} [preorder α] (a : α) :
a ≤ a

The relation ≤ on a preorder is reflexive.

source
theorem le_trans {α : Type u} [preorder α] {a b c : α} :
a ≤ b → b ≤ c → a ≤ c

The relation ≤ on a preorder is transitive.

source
theorem lt_iff_le_not_le {α : Type u} [preorder α] {a b : α} :
a < b ↔ a ≤ b ∧ ¬b ≤ a
source
theorem lt_of_le_not_le {α : Type u} [preorder α] {a b : α} :
a ≤ b → ¬b ≤ a → a < b
source
theorem le_not_le_of_lt {α : Type u} [preorder α] {a b : α} :
a < b → a ≤ b ∧ ¬b ≤ a
source
theorem le_of_eq {α : Type u} [preorder α] {a b : α} :
a = b → a ≤ b
source
theorem ge_trans {α : Type u} [preorder α] {a b c : α} :
a ≥ b → b ≥ c → a ≥ c
source
theorem lt_irrefl {α : Type u} [preorder α] (a : α) :
¬a < a
source
theorem gt_irrefl {α : Type u} [preorder α] (a : α) :
¬a > a
source
theorem lt_trans {α : Type u} [preorder α] {a b c : α} :
a < b → b < c → a < c
source
theorem gt_trans {α : Type u} [preorder α] {a b c : α} :
a > b → b > c → a > c
source
theorem ne_of_lt {α : Type u} [preorder α] {a b : α} (h : a < b) :
a ≠ b
source
theorem ne_of_gt {α : Type u} [preorder α] {a b : α} (h : b < a) :
a ≠ b
source
theorem lt_asymm {α : Type u} [preorder α] {a b : α} (h : a < b) :
¬b < a
source
theorem le_of_lt {α : Type u} [preorder α] {a b : α} :
a < b → a ≤ b
source
theorem lt_of_lt_of_le {α : Type u} [preorder α] {a b c : α} :
a < b → b ≤ c → a < c
source
theorem lt_of_le_of_lt {α : Type u} [preorder α] {a b c : α} :
a ≤ b → b < c → a < c
source
theorem gt_of_gt_of_ge {α : Type u} [preorder α] {a b c : α} (h₁ : a > b) (h₂ : b ≥ c) :
a > c
source
theorem gt_of_ge_of_gt {α : Type u} [preorder α] {a b c : α} (h₁ : a ≥ b) (h₂ : b > c) :
a > c
source
theorem not_le_of_gt {α : Type u} [preorder α] {a b : α} (h : a > b) :
¬a ≤ b
source
theorem not_lt_of_ge {α : Type u} [preorder α] {a b : α} (h : a ≥ b) :
¬a < b
source
theorem le_of_lt_or_eq {α : Type u} [preorder α] {a b : α} :
a < b ∨ a = b → a ≤ b
source
theorem le_of_eq_or_lt {α : Type u} [preorder α] {a b : α} (h : a = b ∨ a < b) :
a ≤ b
source
@[protected, instance]
def decidable_lt_of_decidable_le {α : Type u} [preorder α] [decidable_rel has_le.le] :
decidable_rel has_lt.lt
Equations

Definition of partial_order and lemmas about types with a partial order #

source
@[class]
structure partial_order (α : Type u) :
Type u
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • 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
source
@[instance]
def partial_order.to_preorder (α : Type u) [self : partial_order α] :
preorder α
source
theorem le_antisymm {α : Type u} [partial_order α] {a b : α} :
a ≤ b → b ≤ a → a = b
source
theorem le_antisymm_iff {α : Type u} [partial_order α] {a b : α} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem lt_of_le_of_ne {α : Type u} [partial_order α] {a b : α} :
a ≤ b → a ≠ b → a < b
source
@[protected, instance]
def decidable_eq_of_decidable_le {α : Type u} [partial_order α] [decidable_rel has_le.le] :
decidable_eq α
Equations
source
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
source
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
source
theorem decidable.le_iff_lt_or_eq {α : Type u} [partial_order α] [decidable_rel has_le.le] {a b : α} :
a ≤ b ↔ a < b ∨ a = b
source
theorem lt_or_eq_of_le {α : Type u} [partial_order α] {a b : α} :
a ≤ b → a < b ∨ a = b
source
theorem le_iff_lt_or_eq {α : Type u} [partial_order α] {a b : α} :
a ≤ b ↔ a < b ∨ a = b

Definition of linear_order and lemmas about types with a linear order #

source
def max_default {α : Type u} [has_le α] [decidable_rel has_le.le] (a b : α) :
α

Default definition of max.

Equations
source
def min_default {α : Type u} [has_le α] [decidable_rel has_le.le] (a b : α) :
α

Default definition of min.

Equations
source
@[class]
structure linear_order (α : Type u) :
Type u

A linear order is reflexive, transitive, antisymmetric and total relation ≤. We assume that every linear ordered type has decidable (≤), (<), and (=).

Instances
source
@[instance]
def linear_order.to_partial_order (α : Type u) [self : linear_order α] :
partial_order α
source
theorem le_total {α : Type u} [linear_order α] (a b : α) :
a ≤ b ∨ b ≤ a
source
theorem le_of_not_ge {α : Type u} [linear_order α] {a b : α} :
¬a ≥ b → a ≤ b
source
theorem le_of_not_le {α : Type u} [linear_order α] {a b : α} :
¬a ≤ b → b ≤ a
source
theorem not_lt_of_gt {α : Type u} [linear_order α] {a b : α} (h : a > b) :
¬a < b
source
theorem lt_trichotomy {α : Type u} [linear_order α] (a b : α) :
a < b ∨ a = b ∨ b < a
source
theorem le_of_not_lt {α : Type u} [linear_order α] {a b : α} (h : ¬b < a) :
a ≤ b
source
theorem le_of_not_gt {α : Type u} [linear_order α] {a b : α} :
¬a > b → a ≤ b
source
theorem lt_of_not_ge {α : Type u} [linear_order α] {a b : α} (h : ¬a ≥ b) :
a < b
source
theorem lt_or_le {α : Type u} [linear_order α] (a b : α) :
a < b ∨ b ≤ a
source
theorem le_or_lt {α : Type u} [linear_order α] (a b : α) :
a ≤ b ∨ b < a
source
theorem lt_or_ge {α : Type u} [linear_order α] (a b : α) :
a < b ∨ a ≥ b
source
theorem le_or_gt {α : Type u} [linear_order α] (a b : α) :
a ≤ b ∨ a > b
source
theorem lt_or_gt_of_ne {α : Type u} [linear_order α] {a b : α} (h : a ≠ b) :
a < b ∨ a > b
source
theorem ne_iff_lt_or_gt {α : Type u} [linear_order α] {a b : α} :
a ≠ b ↔ a < b ∨ a > b
source
theorem lt_iff_not_ge {α : Type u} [linear_order α] (x y : α) :
x < y ↔ ¬x ≥ y
source
@[simp]
theorem not_lt {α : Type u} [linear_order α] {a b : α} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem not_le {α : Type u} [linear_order α] {a b : α} :
¬a ≤ b ↔ b < a
source
@[protected, instance]
def has_lt.lt.decidable {α : Type u} [linear_order α] (a b : α) :
decidable (a < b)
Equations
source
@[protected, instance]
def has_le.le.decidable {α : Type u} [linear_order α] (a b : α) :
decidable (a ≤ b)
Equations
source
@[protected, instance]
def eq.decidable {α : Type u} [linear_order α] (a b : α) :
decidable (a = b)
Equations
source
theorem eq_or_lt_of_not_lt {α : Type u} [linear_order α] {a b : α} (h : ¬a < b) :
a = b ∨ b < a
source
@[protected, instance]
def has_le.le.is_total_preorder {α : Type u} [linear_order α] :
is_total_preorder α has_le.le
source
@[protected, instance]
def is_strict_weak_order_of_linear_order {α : Type u} [linear_order α] :
is_strict_weak_order α has_lt.lt
source
@[protected, instance]
def is_strict_total_order_of_linear_order {α : Type u} [linear_order α] :
is_strict_total_order α has_lt.lt
source
def lt_by_cases {α : Type u} [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
  • 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₂ _))
source
theorem le_imp_le_of_lt_imp_lt {α : Type u} [linear_order α] {β : Type u_1} [preorder α] [linear_order β] {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) :
c ≤ d