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 S is_relation ( S , R )
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):
is_transitive ( S , R ) a , b , c . a S b S c S ( a , b ) R ( b , c ) R ( a , c ) 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):
is_reflexive ( S , R ) a . a S { ( a , a ) , R }
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):
is_symmetric ( S , R ) a , b . a S b S ( a , b ) R ( b , a ) 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):
is_equivalence ( S , R ) ( is_relation ( S , R ) is_symmetric ( S , R ) is_reflexive ( S , R ) is_transitive ( S , R ) )
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):
class ( S , R , a ) = { b S | ( a , b ) R }
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):
is_equivalence ( S , R ) a , b . ( a , b ) S × S ( class ( S , R , a ) class ( S , R , b ) = ) ( class ( S , R , a ) = class ( S , R , b ) )
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):
is_reflexive ( S , R ) a . a S a class ( S , R , a )
Signatures:
sts


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