mathlib documentation

order.rel_classes

Unbundled relation classes

In this file we prove some properties of is_* classes defined in init.algebra.classes. The main difference between these classes and the usual order classes (preorder etc) is that usual classes extend has_le and/or has_lt while these classes take a relation as an explicit argument.

theorem is_refl.swap {α : Type u} (r : α → α → Prop) [is_refl α r] :

theorem is_irrefl.swap {α : Type u} (r : α → α → Prop) [is_irrefl α r] :

theorem is_trans.swap {α : Type u} (r : α → α → Prop) [is_trans α r] :

theorem is_antisymm.swap {α : Type u} (r : α → α → Prop) [is_antisymm α r] :

theorem is_asymm.swap {α : Type u} (r : α → α → Prop) [is_asymm α r] :

theorem is_total.swap {α : Type u} (r : α → α → Prop) [is_total α r] :

theorem is_trichotomous.swap {α : Type u} (r : α → α → Prop) [is_trichotomous α r] :

theorem is_preorder.swap {α : Type u} (r : α → α → Prop) [is_preorder α r] :

theorem is_strict_order.swap {α : Type u} (r : α → α → Prop) [is_strict_order α r] :

theorem is_partial_order.swap {α : Type u} (r : α → α → Prop) [is_partial_order α r] :

theorem is_total_preorder.swap {α : Type u} (r : α → α → Prop) [is_total_preorder α r] :

theorem is_linear_order.swap {α : Type u} (r : α → α → Prop) [is_linear_order α r] :

theorem is_asymm.is_antisymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :

theorem is_asymm.is_irrefl {α : Type u} {r : α → α → Prop} [is_asymm α r] :

@[instance]
def has_le.le.is_refl {α : Type u} [preorder α] :

@[instance]
def ge.is_refl {α : Type u} [preorder α] :

@[instance]
def has_le.le.is_trans {α : Type u} [preorder α] :

@[instance]
def ge.is_trans {α : Type u} [preorder α] :

@[instance]
def has_le.le.is_preorder {α : Type u} [preorder α] :

@[instance]
def ge.is_preorder {α : Type u} [preorder α] :

@[instance]
def has_lt.lt.is_irrefl {α : Type u} [preorder α] :

@[instance]
def gt.is_irrefl {α : Type u} [preorder α] :

@[instance]
def has_lt.lt.is_trans {α : Type u} [preorder α] :

@[instance]
def gt.is_trans {α : Type u} [preorder α] :

@[instance]
def has_lt.lt.is_asymm {α : Type u} [preorder α] :

@[instance]
def gt.is_asymm {α : Type u} [preorder α] :

@[instance]
def has_lt.lt.is_antisymm {α : Type u} [preorder α] :

@[instance]
def gt.is_antisymm {α : Type u} [preorder α] :

@[instance]

@[instance]
def gt.is_strict_order {α : Type u} [preorder α] :

@[instance]

@[instance]
def ge.is_antisymm {α : Type u} [partial_order α] :

@[instance]

@[instance]
def ge.is_partial_order {α : Type u} [partial_order α] :

@[instance]
def has_le.le.is_total {α : Type u} [linear_order α] :

@[instance]
def ge.is_total {α : Type u} [linear_order α] :

@[instance]
def ge.is_total_preorder {α : Type u} [linear_order α] :

@[instance]

@[instance]
def ge.is_linear_order {α : Type u} [linear_order α] :

@[instance]

@[instance]
def gt.is_trichotomous {α : Type u} [linear_order α] :

@[instance]

theorem trans_trichotomous_left {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} :
¬r b ar b cr a c

theorem trans_trichotomous_right {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} :
r a b¬r c br a c

def partial_order_of_SO {α : Type u} (r : α → α → Prop) [is_strict_order α r] :

Construct a partial order from a is_strict_order relation

Equations
@[class]
structure is_strict_total_order' (α : Type u) :
(α → α → Prop) → Prop

This is basically the same as is_strict_total_order, but that definition is in Type (probably by mistake) and also has redundant assumptions.

Instances
def linear_order_of_STO' {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] [Π (x y : α), decidable (¬r x y)] :

Construct a linear order from an is_strict_total_order' relation

Equations
theorem is_strict_total_order'.swap {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] :

@[class]
structure is_order_connected (α : Type u) :
(α → α → Prop) → Prop
  • conn : ∀ (a b c : α), lt a clt a b lt b c

A connected order is one satisfying the condition a < c → a < b ∨ b < c. This is recognizable as an intuitionistic substitute for a ≤ b ∨ b ≤ a on the constructive reals, and is also known as negative transitivity, since the contrapositive asserts transitivity of the relation ¬ a < b.

Instances
theorem is_order_connected.neg_trans {α : Type u} {r : α → α → Prop} [is_order_connected α r] {a b c : α} :
¬r a b¬r b c¬r a c

theorem is_strict_weak_order_of_is_order_connected {α : Type u} {r : α → α → Prop} [is_asymm α r] [is_order_connected α r] :

@[instance]
def is_order_connected_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

@[instance]
def is_strict_total_order_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

@[instance]

@[class]
structure is_extensional (α : Type u) :
(α → α → Prop) → Prop
  • ext : ∀ (a b : α), (∀ (x : α), r x a r x b)a = b

An extensional relation is one in which an element is determined by its set of predecessors. It is named for the x ∈ y relation in set theory, whose extensionality is one of the first axioms of ZFC.

Instances
@[instance]
def is_extensional_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

@[instance]
def is_well_order.is_strict_total_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

@[instance]
def is_well_order.is_extensional {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

@[instance]
def is_well_order.is_trichotomous {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

@[instance]
def is_well_order.is_trans {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

@[instance]
def is_well_order.is_irrefl {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

@[instance]
def is_well_order.is_asymm {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :

def is_well_order.linear_order {α : Type u} (r : α → α → Prop) [is_well_order α r] :

Construct a decidable linear order from a well-founded linear order.

Equations
@[instance]
def sum.lex.is_well_order {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
is_well_order β) (sum.lex r s)

@[instance]
def prod.lex.is_well_order {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [is_well_order α r] [is_well_order β s] :
is_well_order × β) (prod.lex r s)

def unbounded {α : Type u} :
(α → α → Prop)set α → Prop

An unbounded or cofinal set

Equations
def bounded {α : Type u} :
(α → α → Prop)set α → Prop

A bounded or final set

Equations
  • bounded r s = ∃ (a : α), ∀ (b : α), b sr b a
@[simp]
theorem not_bounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :

@[simp]
theorem not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :