# OpenMath Content Dictionary: relation3

Canonical URL:
http://www.openmath.org/cd/relation3.ocd
CD Base:
http://www.openmath.org/cd
CD File:
relation3.ocd
CD as XML Encoded OpenMath:
relation3.omcd
Defines:
class, classes, equivalence_closure, is_equivalence, is_reflexive, is_relation, is_symmetric, is_transitive, reflexive_closure, symmetric_closure, transitive_closure
Date:
2001-03-12
Version:
2
Review Date:
2003-04-01
Status:
official

  Author: OpenMath Consortium
SourceURL: https://github.com/OpenMath/CDs


This CD holds the basic equivalence relation notions.

## is_relation

Description:

This symbol is a boolean function of two arguments, S and R. The first argument should be a set. When applied to S and R, the function returns true if and only if the second argument is a subset of the Cartesian product of S with itself.

Commented Mathematical property (CMP):
R a subset of S x S if and only if is_relation (S,R).
Formal Mathematical property (FMP):
$R\subset S\equiv \mathrm{is_relation}\left(S,R\right)$
Signatures:
sts

 [Next: equivalence_closure] [Last: classes] [Top]

## equivalence_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest equivalence relation (with respect to inclusion) on S containing R.

Signatures:
sts

 [Next: transitive_closure] [Previous: is_relation] [Top]

## transitive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest transitive relation (with respect to inclusion) on S containing R.

Signatures:
sts

 [Next: reflexive_closure] [Previous: equivalence_closure] [Top]

## reflexive_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest reflexive relation (with respect to inclusion) on S containing R.

Signatures:
sts

 [Next: symmetric_closure] [Previous: transitive_closure] [Top]

## symmetric_closure

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the smallest symmetric relation (with respect to inclusion) on S containing R.

Signatures:
sts

 [Next: is_transitive] [Previous: reflexive_closure] [Top]

## is_transitive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a transitive relation on the first.

Commented Mathematical property (CMP):
R is transitive on S if and only if, for all a,b,c in S with (a,b) in R and (b,c) in R, wehave (a,c) in R.
Formal Mathematical property (FMP):
$\mathrm{is_transitive}\left(S,R\right)\equiv \forall a,b,c.a\in S\wedge b\in S\wedge c\in S\wedge \left(a,b\right)\in R\wedge \left(b,c\right)\in R⇒\left(a,c\right)\in R$
Signatures:
sts

 [Next: is_reflexive] [Previous: symmetric_closure] [Top]

## is_reflexive

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a reflexive relation on the first.

Commented Mathematical property (CMP):
is_reflexive(S,R) if and only if, for all, a in S, we have (a,a) in R.
Formal Mathematical property (FMP):
$\mathrm{is_reflexive}\left(S,R\right)\equiv \forall a.a\in S⇒\left\{\left(a,a\right),R\right\}$
Signatures:
sts

 [Next: is_symmetric] [Previous: is_transitive] [Top]

## is_symmetric

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first.

Commented Mathematical property (CMP):
is_symmetric(S,R) if and only if, for all a, b in S with (a,b) in R, we have (b,a) in R.
Formal Mathematical property (FMP):
$\mathrm{is_symmetric}\left(S,R\right)\equiv \forall a,b.a\in S\wedge b\in S\wedge \left(a,b\right)\in R⇒\left(b,a\right)\in R$
Signatures:
sts

 [Next: is_equivalence] [Previous: is_reflexive] [Top]

## is_equivalence

Description:

This symbol represents the boolean binary function which returns true if and only if the second argument is an equivalence relation on the first.

Commented Mathematical property (CMP):
R is an equivalence relation on S if and only if R is a symmetric, reflexive, transitive relation on S.
Formal Mathematical property (FMP):
$\mathrm{is_equivalence}\left(S,R\right)\equiv \left(\mathrm{is_relation}\left(S,R\right)\wedge \mathrm{is_symmetric}\left(S,R\right)\wedge \mathrm{is_reflexive}\left(S,R\right)\wedge \mathrm{is_transitive}\left(S,R\right)\right)$
Signatures:
sts

 [Next: class] [Previous: is_symmetric] [Top]

## class

Description:

This symbol represents a ternary function whose first argument is a set S, whose second argument is a relation R on S, and whose third argument is an element a of S. When applied to S, R, and a, it represents the set of all elements in S related to a by R, that is, the set {b in S | (a,b) in R}.

Commented Mathematical property (CMP):
class(S,R,a) = {b in S | (a,b) in R}.
Formal Mathematical property (FMP):
$\mathrm{class}\left(S,R,a\right)=\left\{b\in S|\left(a,b\right)\in R\right\}$
Signatures:
sts

 [Next: classes] [Previous: is_equivalence] [Top]

## classes

Description:

This symbol represents a binary function whose first argument is a set S, whose second argument is a relation R on S. When applied to S and R, it represents the set of all elements in S of the form class(S,R,a) for a in S.

Commented Mathematical property (CMP):
The classes of an equivalence relation R on S partition S.
Formal Mathematical property (FMP):
$\mathrm{is_equivalence}\left(S,R\right)⇒\forall a,b.\left(a,b\right)\in S×S⇒\left(\mathrm{class}\left(S,R,a\right)\cap \mathrm{class}\left(S,R,b\right)=\varnothing \right)\vee \left(\mathrm{class}\left(S,R,a\right)=\mathrm{class}\left(S,R,b\right)\right)$
Commented Mathematical property (CMP):
The classes of a reflexive relation R on S cover S, as a in S belongs to class(S,R,a).
Formal Mathematical property (FMP):
$\mathrm{is_reflexive}\left(S,R\right)⇒\forall a.a\in S⇒a\in \mathrm{class}\left(S,R,a\right)$
Signatures:
sts

 [First: is_relation] [Previous: class] [Top]