Relations: Definitions

References

• Term Rewriting and All That
• Simple Laws about Nonprominent Properties of Binary Relations
• [Applied Combinatorics][KellerTrotter2017]

Operations on relations

def Relation.emptyHRelation {α : Sort u} {β : Sort v} : α → β → Prop

The empty (heterogeneous) relation, which always returns False.

def Relation.dom {α : Type u_1} {β : Sort u_2} (r : α → β → Prop) : Set α

Domain of a relation.

def Relation.cod {α : Sort u_1} {β : Type u_2} (r : α → β → Prop) : Set β

Codomain of a relation, aka range.

def Relation.Join₂ {α : Sort u_1} (r₁ r₂ : α → α → Prop) (a b : α) : Prop

Generalisation of Join to two relations.

@[reducible, inline, deprecated "use `Join (ReflTrasnGen ·)` instead" (since := "2026-09-12")]

abbrev Relation.MJoin {α : Type u_1} (r : α → α → Prop) : α → α → Prop

The join of the reflexive transitive closure. This is not named in Mathlib, but see #loogle Relation.Join (Relation.ReflTransGen ?r)

def Relation.UpTo {α : Type u_1} (r s : α → α → Prop) : α → α → Prop

The relation r 'up to' the relation s.

def Relation.Preserves {α : Sort u_1} (r : α → α → Prop) (P : α → Prop) : Prop

Relation r preserves predicate P.

Confluence and commutation properties

@[reducible, inline]

abbrev Relation.Diamond {α : Type u_1} (r : α → α → Prop) : Prop

A relation has the diamond property when all reductions with a common origin are joinable

@[reducible, inline]

abbrev Relation.DiamondCommute {α : Sort u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of Diamond to two relations.

@[reducible, inline]

abbrev Relation.Confluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is confluent when its reflexive transitive closure has the diamond property.

@[reducible, inline]

abbrev Relation.Commute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of Confluent to two relations.

@[reducible, inline]

abbrev Relation.SemiConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is semi-confluent when single and multiple steps with common origin are multi-joinable.

@[reducible, inline]

abbrev Relation.SemiCommute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalisation of SemiConfluent to two relations.

@[reducible, inline]

abbrev Relation.ChurchRosser {α : Type u_1} (r : α → α → Prop) : Prop

A relation has the Church Rosser property when equivalence implies multi-joinability.

@[reducible, inline]

abbrev Relation.LocallyConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is locally confluent when all reductions with a common origin are multi-joinable

def Relation.LocallyCommute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of LocallyConfluent to two relations.

@[reducible, inline]

abbrev Relation.StronglyConfluent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is strongly confluent when single steps are reflexive- and multi-joinable.

def Relation.StronglyCommute {α : Type u_1} (r₁ r₂ : α → α → Prop) : Prop

Generalization of StronglyConfluent to two relations.

Normalization properties

@[reducible, inline]

abbrev Relation.Reducible {α : Sort u_1} (r : α → α → Prop) (x : α) : Prop

An element is reducible with respect to a relation if there is a value it is related to.

@[reducible, inline]

abbrev Relation.Normal {α : Sort u_1} (r : α → α → Prop) (x : α) : Prop

An element is normal if it is not reducible.

@[reducible, inline]

abbrev Relation.Normalizable {α : Type u_1} (r : α → α → Prop) (x : α) : Prop

An element is normalizable if it is related to a normal element.

@[reducible, inline]

abbrev Relation.Normalizing {α : Type u_1} (r : α → α → Prop) : Prop

A relation is normalizing when every element is normalizable.

@[reducible, inline]

abbrev Relation.SN {α : Sort u_1} (r : α → α → Prop) : α → Prop

An element x is SN (for strongly-normalising) for a relation r if it is accessible under the inverse of r.

@[reducible, inline]

abbrev Relation.Terminating {α : Sort u_1} (r : α → α → Prop) : Prop

A relation is terminating when the inverse of its transitive closure is well-founded. Note that this is also called Noetherian or strongly normalizing in the literature.

@[reducible, inline]

abbrev Relation.Acyclic {α : Sort u_1} (r : α → α → Prop) : Prop

A relation is acyclic if its transitive closure is irreflexive, equivalently if it admits no nonempty cycle.

@[reducible, inline]

abbrev Relation.Convergent {α : Type u_1} (r : α → α → Prop) : Prop

A relation is convergent when it is both confluent and terminating.

Modal properties

class Relation.RightEuclidean {α : Sort u_1} (r : α → α → Prop) : Prop

A relation r is (right) Euclidean if r a b and r a c guarantee r b c.

• rightEuclidean {a b c : α} : r a b → r a c → r b c

class Relation.LeftEuclidean {α : Sort u_1} (r : α → α → Prop) : Prop

A relation r is (left) Euclidean if r a c and r b c guarantee r a b.

• leftEuclidean {a b c : α} : r a c → r b c → r a b

class Relation.Serial {α : Sort u_1} (r : α → α → Prop) : Prop

A relation r is serial if every element is Reducible, i.e. Relator.LeftTotal.

• serial : Relator.LeftTotal r

Relations and sets in the underlying types

@[reducible, inline]

abbrev Relation.successors {α : Sort u_1} {β : Type u_2} (r : α → β → Prop) (a : α) : Set β

The set of successors of an element a in a relation r.

@[reducible, inline]

abbrev Relation.predecessors {α : Type u_1} {β : Sort u_2} (r : α → β → Prop) (b : β) : Set α

The set of predecessors of an element b in a relation r.

def Relation.restrict {α : Type u_1} (r : α → α → Prop) (s : Set α) : α → α → Prop

The restriction of a relation r to a set s.

Interval order

def Relation.IsIntervalOrder {α : Sort u_1} (r : α → α → Prop) : Prop

Fishburn's theorem (see sections 6.6 and 6.7 of [KellerTrotter2017]) shows that the definition below is a sufficient and necessary condition for a relation r to have a representation by closed intervals on the real line such that r i1 i2 iff the right endpoint of i1 is less than the left endpoint of i2.

Properties of relations on restrictions of their (co)domain

@[instance_reducible]

instance Set.instCoeDepForallForallPropForallElemForall_cslib {α : Type u_1} (r : α → α → Prop) (s : Set α) : CoeDep (α → α → Prop) r (↑s → ↑s → Prop)

def Set.ReflOn {α : Type u_1} (s : Set α) (r : α → α → Prop) : Prop

ReflOn s r is true when a relation r is reflexive on its restriction to a set s.

@[reducible, inline]

abbrev Set.LeftQuasiRefl {α : Type u_1} (r : α → α → Prop) : Prop

LeftQuasiRefl r is true when a relation r is reflexive on its domain.

@[reducible, inline]

abbrev Set.RightQuasiRefl {α : Type u_1} (r : α → α → Prop) : Prop

RightQuasiRefl r is true when a relation r is reflexive on its codomain.

def Set.SymmOn {α : Type u_1} (s : Set α) (r : α → α → Prop) : Prop

SymmOn s r is true when a relation r is symmetric on its restriction to a set s.