Relations: Definitions

References

• Term Rewriting and All That
• Simple Laws about Nonprominent Properties of Binary Relations

Operations on relations

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

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

Equations

• Relation.emptyHRelation x✝¹ x✝ = False

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

Domain of a relation.

Equations

• Relation.dom r = {a : α | ∃ (b : β), r a b}

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

Codomain of a relation, aka range.

Equations

• Relation.cod r = {b : β | ∃ (a : α), r a b}

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

Generalisation of Join to two relations.

Equations

• Relation.Join₂ r₁ r₂ a b = ∃ (c : α), r₁ a c ∧ r₂ b c

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

Equations

• Relation.MJoin r = Relation.Join (Relation.ReflTransGen r)

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

The relation r 'up to' the relation s.

Equations

• Relation.UpTo r s = Relation.Comp s (Relation.Comp r s)

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

Relation r preserves predicate P.

Equations

• Relation.Preserves r P = ∀ ⦃a b : α⦄, r a b → P a → P b

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

Equations

• Relation.Diamond r = ∀ {a b c : α}, r a b → r a c → Relation.Join r b c

@[reducible, inline]

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

Generalization of Diamond to two relations.

Equations

• Relation.DiamondCommute r₁ r₂ = ∀ {x y₁ y₂ : α}, r₁ x y₁ → r₂ x y₂ → Relation.Join₂ r₂ r₁ y₁ y₂

@[reducible, inline]

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

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

Equations

• Relation.Confluent r = Relation.Diamond (Relation.ReflTransGen r)

@[reducible, inline]

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

Generalization of Confluent to two relations.

Equations

• Relation.Commute r₁ r₂ = Relation.DiamondCommute (Relation.ReflTransGen r₁) (Relation.ReflTransGen r₂)

@[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.

Equations

• Relation.SemiConfluent r = ∀ {x y₁ y₂ : α}, r x y₁ → Relation.ReflTransGen r x y₂ → Relation.Join (Relation.ReflTransGen r) y₁ y₂

@[reducible, inline]

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

Generalisation of SemiConfluent to two relations.

Equations

• Relation.SemiCommute r₁ r₂ = ∀ {x y₁ y₂ : α}, r₁ x y₁ → Relation.ReflTransGen r₂ x y₂ → Relation.Join₂ (Relation.ReflTransGen r₂) (Relation.ReflTransGen r₁) y₁ y₂

@[reducible, inline]

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

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

Equations

• Relation.ChurchRosser r = ∀ {x y : α}, Relation.EqvGen r x y → Relation.Join (Relation.ReflTransGen r) x y

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

Equations

• Relation.LocallyConfluent r = ∀ {a b c : α}, r a b → r a c → Relation.Join (Relation.ReflTransGen r) b c

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

Generalization of LocallyConfluent to two relations.

Equations

• Relation.LocallyCommute r₁ r₂ = ∀ {a b c : α}, r₁ a b → r₂ a c → Relation.Join₂ (Relation.ReflTransGen r₂) (Relation.ReflTransGen r₁) b c

@[reducible, inline]

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

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

Equations

• Relation.StronglyConfluent r = ∀ {x y₁ y₂ : α}, r x y₁ → r x y₂ → ∃ (z : α), Relation.ReflGen r y₁ z ∧ Relation.ReflTransGen r y₂ z

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

Generalization of StronglyConfluent to two relations.

Equations

• Relation.StronglyCommute r₁ r₂ = ∀ {x y₁ y₂ : α}, r₁ x y₁ → r₂ x y₂ → ∃ (z : α), Relation.ReflGen r₂ y₁ z ∧ Relation.ReflTransGen r₁ y₂ z

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.

Equations

• Relation.Reducible r x = ∃ (y : α), r x y

@[reducible, inline]

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

An element is normal if it is not reducible.

Equations

• Relation.Normal r x = ¬Relation.Reducible r x

@[reducible, inline]

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

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

Equations

• Relation.Normalizable r x = ∃ (n : α), Relation.ReflTransGen r x n ∧ Relation.Normal r n

@[reducible, inline]

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

A relation is normalizing when every element is normalizable.

Equations

• Relation.Normalizing r = ∀ (x : α), Relation.Normalizable r x

@[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.

Equations

• Relation.SN r = Acc fun (a b : α) => r b a

@[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.

Equations

• Relation.Terminating r = WellFounded fun (a b : α) => r b a

@[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.

Equations

• Relation.Acyclic r = Std.Irrefl (Relation.TransGen r)

@[reducible, inline]

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

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

Equations

• Relation.Convergent r = (Relation.Confluent r ∧ Relation.Terminating r)

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

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)

Equations

• Set.instCoeDepForallForallPropForallElemForall_cslib r s = { coe := fun (a b : ↑s) => r a.val b.val }

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.

Equations

• s.ReflOn r = ∀ (a : α), a ∈ s → r a a

@[reducible, inline]

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

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

Equations

• Set.LeftQuasiRefl r = (Relation.dom r).ReflOn r

@[reducible, inline]

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

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

Equations

• Set.RightQuasiRefl r = (Relation.cod r).ReflOn r

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.

Equations

• s.SymmOn r = ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → r a b → r b a