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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
@[instance]
def preorder.is_total_preorder {α : Type u} [preorder α] [is_total α has_le.le] :
is_total_preorder α has_le.le

source
@[instance]
def has_le.le.is_antisymm {α : Type u} [partial_order α] :
is_antisymm α has_le.le

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

source
@[instance]
def has_le.le.is_partial_order {α : Type u} [partial_order α] :
is_partial_order α has_le.le

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

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

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

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

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

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

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

source
@[instance]
def has_lt.lt.is_trichotomous {α : Type u} [linear_order α] :
is_trichotomous α has_lt.lt

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

source
theorem trans_trichotomous_left {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} (a_1 : ¬r b a) (a_2 : r b c) :
r a c

source
theorem trans_trichotomous_right {α : Type u} {r : α → α → Prop} [is_trans α r] [is_trichotomous α r] {a b c : α} (a_1 : r a b) (a_2 : ¬r c b) :
r a c

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

Construct a partial order from a is_strict_order relation

Equations
source
@[class]
structure is_strict_total_order' (α : Type u) (lt : α → α → 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
source
def linear_order_of_STO' {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] :
linear_order α

Construct a linear order from a is_strict_total_order' relation

Equations
source
def decidable_linear_order_of_STO' {α : Type u} (r : α → α → Prop) [is_strict_total_order' α r] [decidable_rel r] :
decidable_linear_order α

Construct a decidable linear order from a is_strict_total_order' relation

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

source
@[instance]
def has_lt.lt.is_strict_total_order' {α : Type u} [linear_order α] :
is_strict_total_order' α has_lt.lt

source
@[class]
structure is_order_connected (α : Type u) (lt : α → α → Prop) :
Prop
  • conn : ∀ (a b c : α), lt a c → lt 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
source
theorem is_order_connected.neg_trans {α : Type u} {r : α → α → Prop} [is_order_connected α r] {a b c : α} (h₁ : ¬r a b) (h₂ : ¬r b c) :
¬r a c

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

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

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

source
@[instance]
def has_lt.lt.is_strict_total_order {α : Type u} [linear_order α] :
is_strict_total_order α has_lt.lt

source
@[instance]
def has_lt.lt.is_order_connected {α : Type u} [linear_order α] :
is_order_connected α has_lt.lt

source
@[instance]
def has_lt.lt.is_incomp_trans {α : Type u} [linear_order α] :
is_incomp_trans α has_lt.lt

source
@[instance]
def has_lt.lt.is_strict_weak_order {α : Type u} [linear_order α] :
is_strict_weak_order α has_lt.lt

source
@[class]
structure is_extensional (α : Type u) (r : α → α → 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
source
@[instance]
def is_extensional_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :
is_extensional α r

source
@[class]
structure is_well_order (α : Type u) (r : α → α → Prop) :
Prop

A well order is a well-founded linear order.

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

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

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

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

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

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

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

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

Equations
source
@[instance]
def empty_relation.is_well_order {α : Type u} [subsingleton α] :
is_well_order α empty_relation

source
@[instance]
def nat.lt.is_well_order  :
is_well_order ℕ has_lt.lt

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

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

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

An unbounded or cofinal set

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

A bounded or final set

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

source
@[simp]
theorem not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :
¬unbounded r s ↔ bounded r s

source
theorem well_founded.has_min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (s : set α) (a : s.nonempty) :
∃ (a : α) (H : a ∈ s), ∀ (x : α), x ∈ s → ¬r x a

If r is a well-founded relation, then any nonempty set has a minimal element with respect to r.

source
def well_founded.min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) :
α

A minimal element of a nonempty set in a well-founded order

Equations
source
theorem well_founded.min_mem {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) :
H.min p h ∈ p

source
theorem well_founded.not_lt_min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) {x : α} (xp : x ∈ p) :
¬r x (H.min p h)

source
theorem well_founded.well_founded_iff_has_min {α : Type u_1} {r : α → α → Prop} :
well_founded r ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → ¬r x m)

source
theorem well_founded.eq_iff_not_lt_of_le {α : Type u_1} [partial_order α] {x y : α} :
x ≤ y → y = x ↔ ¬x < y

source
theorem well_founded.well_founded_iff_has_max' {α : Type u} [partial_order α] :
well_founded gt ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → m ≤ x → x = m)

source
theorem well_founded.well_founded_iff_has_min' {α : Type u} [partial_order α] :
well_founded has_lt.lt ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → x ≤ m → x = m)

source
def well_founded.sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (s : set α) (h : bounded r s) :
α

The supremum of a bounded, well-founded order

Equations
  • wf.sup s h = wf.min {x : α | ∀ (a : α), a ∈ s → r a x} h
source
theorem well_founded.lt_sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) {s : set α} (h : bounded r s) {x : α} (hx : x ∈ s) :
r x (wf.sup s h)

source
def well_founded.succ {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (x : α) :
α

A successor of an element x in a well-founded order is a minimal element y such that x < y if one exists. Otherwise it is x itself.

Equations
  • wf.succ x = dite (∃ (y : α), r x y) (λ (h : ∃ (y : α), r x y), wf.min {y : α | r x y} h) (λ (h : ¬∃ (y : α), r x y), x)
source
theorem well_founded.lt_succ {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) {x : α} (h : ∃ (y : α), r x y) :
r x (wf.succ x)

source
theorem well_founded.lt_succ_iff {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] {x : α} (h : ∃ (y : α), r x y) (y : α) :
r y (is_well_order.wf.succ x) ↔ r y x ∨ y = x