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 of_eq {α : Type u} {r : α → α → Prop} [is_refl α r] {a b : α} :
a = br a b
theorem comm {α : Type u} {r : α → α → Prop} [is_symm α r] {a b : α} :
r a b r b a
theorem antisymm' {α : Type u} {r : α → α → Prop} [is_antisymm α r] {a b : α} :
r a br b ab = a
theorem antisymm_iff {α : Type u} {r : α → α → Prop} [is_refl α r] [is_antisymm α r] {a b : α} :
r a b r b a a = b
theorem antisymm_of {α : Type u} (r : α → α → Prop) [is_antisymm α r] {a b : α} :
r a br b aa = b

A version of antisymm with r explicit.

This lemma matches the lemmas from lean core in init.algebra.classes, but is missing there.

theorem antisymm_of' {α : Type u} (r : α → α → Prop) [is_antisymm α r] {a b : α} :
r a br b ab = a

A version of antisymm' with r explicit.

This lemma matches the lemmas from lean core in init.algebra.classes, but is missing there.

theorem comm_of {α : Type u} (r : α → α → Prop) [is_symm α r] {a b : α} :
r a b r b a

A version of comm with r explicit.

This lemma matches the lemmas from lean core in init.algebra.classes, but is missing there.

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] :
@[protected]
theorem is_asymm.is_antisymm {α : Type u} (r : α → α → Prop) [is_asymm α r] :
@[protected]
theorem is_asymm.is_irrefl {α : Type u} {r : α → α → Prop} [is_asymm α r] :
@[protected]
theorem is_total.is_trichotomous {α : Type u} (r : α → α → Prop) [is_total α r] :
@[protected, instance]
def is_total.to_is_refl {α : Type u} (r : α → α → Prop) [is_total α r] :
is_refl α r
theorem ne_of_irrefl {α : Type u} {r : α → α → Prop} [is_irrefl α r] {x y : α} :
r x yx y
theorem ne_of_irrefl' {α : Type u} {r : α → α → Prop} [is_irrefl α r] {x y : α} :
r x yy x
theorem not_rel {α : Type u} (r : α → α → Prop) [is_irrefl α r] [subsingleton α] (x y : α) :
¬r x y
@[simp]
theorem empty_relation_apply {α : Type u} (a b : α) :
theorem eq_empty_relation {α : Type u} (r : α → α → Prop) [is_irrefl α r] [subsingleton α] :
@[protected, 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
theorem transitive_of_trans {α : Type u} (r : α → α → Prop) [is_trans α r] :
def partial_order_of_SO {α : Type u} (r : α → α → Prop) [is_strict_order α r] :

Construct a partial order from a is_strict_order relation.

See note [reducible non-instances].

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

This is basically the same as is_strict_total_order, but that definition has a redundant assumption is_incomp_trans α lt.

Instances of this typeclass
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.

See note [reducible non-instances].

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

Order connection #

@[class]
structure is_order_connected (α : Type u) (lt : α → α → 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 of this typeclass
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
theorem is_strict_weak_order_of_is_order_connected {α : Type u} {r : α → α → Prop} [is_asymm α r] [is_order_connected α r] :
@[protected, instance]
def is_order_connected_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :
@[protected, instance]
def is_strict_total_order_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

Extensional relation #

@[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 of this typeclass
@[protected, instance]
def is_extensional_of_is_strict_total_order' {α : Type u} {r : α → α → Prop} [is_strict_total_order' α r] :

Well-order #

@[protected, instance]
def is_well_order.is_strict_total_order {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
@[protected, instance]
def is_well_order.is_extensional {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
@[protected, instance]
def is_well_order.is_trichotomous {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
@[protected, instance]
def is_well_order.is_trans {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
@[protected, instance]
def is_well_order.is_irrefl {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
@[protected, instance]
def is_well_order.is_asymm {α : Type u_1} (r : α → α → Prop) [is_well_order α r] :
noncomputable 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

Derive a has_well_founded instance from a is_well_order instance.

Equations
theorem subsingleton.is_well_order {α : Type u} [subsingleton α] (r : α → α → Prop) [hr : is_irrefl α r] :
@[protected, instance]
@[protected, instance]
def is_empty.is_well_order {α : Type u} [is_empty α] (r : α → α → Prop) :
@[protected, 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 set.unbounded {α : Type u} (r : α → α → Prop) (s : set α) :
Prop

An unbounded or cofinal set.

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

A bounded or final set. Not to be confused with metric.bounded.

Equations
@[simp]
theorem set.not_bounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :
@[simp]
theorem set.not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : set α) :
theorem set.unbounded_of_is_empty {α : Type u} [is_empty α] {r : α → α → Prop} (s : set α) :
@[protected, instance]
def prod.is_refl_preimage_fst {α : Type u} {r : α → α → Prop} [h : is_refl α r] :
@[protected, instance]
def prod.is_refl_preimage_snd {α : Type u} {r : α → α → Prop} [h : is_refl α r] :
@[protected, instance]
def prod.is_trans_preimage_fst {α : Type u} {r : α → α → Prop} [h : is_trans α r] :
@[protected, instance]
def prod.is_trans_preimage_snd {α : Type u} {r : α → α → Prop} [h : is_trans α r] :

Strict-non strict relations #

@[class]
structure is_nonstrict_strict_order (α : Type u_1) (r s : α → α → Prop) :
Type
  • right_iff_left_not_left : ∀ (a b : α), s a b r a b ¬r b a

An unbundled relation class stating that r is the nonstrict relation corresponding to the strict relation s. Compare preorder.lt_iff_le_not_le. This is mostly meant to provide dot notation on (⊆) and (⊂).

Instances of this typeclass
Instances of other typeclasses for is_nonstrict_strict_order
  • is_nonstrict_strict_order.has_sizeof_inst
theorem right_iff_left_not_left {α : Type u} {r s : α → α → Prop} [is_nonstrict_strict_order α r s] {a b : α} :
s a b r a b ¬r b a
theorem right_iff_left_not_left_of {α : Type u} (r s : α → α → Prop) [is_nonstrict_strict_order α r s] {a b : α} :
s a b r a b ¬r b a

A version of right_iff_left_not_left with explicit r and s.

@[protected, nolint, instance]
def is_nonstrict_strict_order.to_is_irrefl {α : Type u} {r s : α → α → Prop} [is_nonstrict_strict_order α r s] :

and #

theorem subset_refl {α : Type u} [has_subset α] [is_refl α has_subset.subset] (a : α) :
a a
theorem subset_rfl {α : Type u} [has_subset α] {a : α} [is_refl α has_subset.subset] :
a a
theorem subset_of_eq {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = ba b
theorem superset_of_eq {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = bb a
theorem ne_of_not_subset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
¬a ba b
theorem ne_of_not_superset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
¬a bb a
theorem subset_trans {α : Type u} [has_subset α] [is_trans α has_subset.subset] {a b c : α} :
a bb ca c
theorem subset_antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a b) (h' : b a) :
a = b
theorem superset_antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a b) (h' : b a) :
b = a
theorem eq.subset' {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = ba b

Alias of subset_of_eq.

theorem eq.superset {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] :
a = bb a

Alias of superset_of_eq.

theorem has_subset.subset.trans {α : Type u} [has_subset α] [is_trans α has_subset.subset] {a b c : α} :
a bb ca c

Alias of subset_trans.

theorem has_subset.subset.antisymm {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a b) (h' : b a) :
a = b

Alias of subset_antisymm.

theorem has_subset.subset.antisymm' {α : Type u} [has_subset α] {a b : α} [is_antisymm α has_subset.subset] (h : a b) (h' : b a) :
b = a

Alias of superset_antisymm.

theorem subset_antisymm_iff {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] [is_antisymm α has_subset.subset] :
a = b a b b a
theorem superset_antisymm_iff {α : Type u} [has_subset α] {a b : α} [is_refl α has_subset.subset] [is_antisymm α has_subset.subset] :
a = b b a a b
theorem ssubset_irrefl {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] (a : α) :
¬a a
theorem ssubset_irrfl {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a : α} :
¬a a
theorem ne_of_ssubset {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ba b
theorem ne_of_ssuperset {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a bb a
theorem ssubset_trans {α : Type u} [has_ssubset α] [is_trans α has_ssubset.ssubset] {a b c : α} :
a bb ca c
theorem ssubset_asymm {α : Type u} [has_ssubset α] [is_asymm α has_ssubset.ssubset] {a b : α} (h : a b) :
¬b a
theorem has_ssubset.ssubset.false {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a : α} :
¬a a

Alias of ssubset_irrfl.

theorem has_ssubset.ssubset.ne {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a ba b

Alias of ne_of_ssubset.

theorem has_ssubset.ssubset.ne' {α : Type u} [has_ssubset α] [is_irrefl α has_ssubset.ssubset] {a b : α} :
a bb a

Alias of ne_of_ssuperset.

theorem has_ssubset.ssubset.trans {α : Type u} [has_ssubset α] [is_trans α has_ssubset.ssubset] {a b c : α} :
a bb ca c

Alias of ssubset_trans.

theorem has_ssubset.ssubset.asymm {α : Type u} [has_ssubset α] [is_asymm α has_ssubset.ssubset] {a b : α} (h : a b) :
¬b a

Alias of ssubset_asymm.

theorem subset_of_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h : a b) :
a b
theorem ssubset_of_subset_not_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} (h₁ : a b) (h₂ : ¬b a) :
a b
theorem ssubset_of_subset_of_ssubset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a b) (h₂ : b c) :
a c
theorem ssubset_of_ssubset_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b c : α} [is_trans α has_subset.subset] (h₁ : a b) (h₂ : b c) :
a c
theorem ssubset_of_subset_of_ne {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a b) (h₂ : a b) :
a b
theorem ssubset_of_ne_of_subset {α : Type u} [has_subset α] [has_ssubset α] [is_nonstrict_strict_order α has_subset.subset has_ssubset.ssubset] {a b : α} [is_antisymm α has_subset.subset] (h₁ : a b) (h₂ : a b) :
a b

Conversion of bundled order typeclasses to unbundled relation typeclasses #

@[protected, instance]
def has_le.le.is_refl {α : Type u} [preorder α] :
@[protected, instance]
def ge.is_refl {α : Type u} [preorder α] :
@[protected, instance]
def has_le.le.is_trans {α : Type u} [preorder α] :
@[protected, instance]
def ge.is_trans {α : Type u} [preorder α] :
@[protected, instance]
def has_le.le.is_preorder {α : Type u} [preorder α] :
@[protected, instance]
def ge.is_preorder {α : Type u} [preorder α] :
@[protected, instance]
def has_lt.lt.is_irrefl {α : Type u} [preorder α] :
@[protected, instance]
def gt.is_irrefl {α : Type u} [preorder α] :
@[protected, instance]
def has_lt.lt.is_trans {α : Type u} [preorder α] :
@[protected, instance]
def gt.is_trans {α : Type u} [preorder α] :
@[protected, instance]
def has_lt.lt.is_asymm {α : Type u} [preorder α] :
@[protected, instance]
def gt.is_asymm {α : Type u} [preorder α] :
@[protected, instance]
def has_lt.lt.is_antisymm {α : Type u} [preorder α] :
@[protected, instance]
def gt.is_antisymm {α : Type u} [preorder α] :
@[protected, instance]
@[protected, instance]
def gt.is_strict_order {α : Type u} [preorder α] :
@[protected, instance]
@[protected, instance]
def ge.is_antisymm {α : Type u} [partial_order α] :
@[protected, instance]
@[protected, instance]
def ge.is_partial_order {α : Type u} [partial_order α] :
@[protected, instance]
def has_le.le.is_total {α : Type u} [linear_order α] :
@[protected, instance]
def ge.is_total {α : Type u} [linear_order α] :
@[protected, instance]
@[protected, instance]
def ge.is_total_preorder {α : Type u} [linear_order α] :
@[protected, instance]
@[protected, instance]
def ge.is_linear_order {α : Type u} [linear_order α] :
@[protected, instance]
@[protected, instance]
def gt.is_trichotomous {α : Type u} [linear_order α] :
@[protected, instance]
@[protected, instance]
def ge.is_trichotomous {α : Type u} [linear_order α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem transitive_le {α : Type u} [preorder α] :
theorem transitive_lt {α : Type u} [preorder α] :
theorem transitive_ge {α : Type u} [preorder α] :
theorem transitive_gt {α : Type u} [preorder α] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]