relation3 http://www.openmath.org/cd/relation3.ocd 2003-04-01 2001-03-12 2 0 official arith1 logic1 nums1 set1 relation1 This CD holds the basic equivalence relation notions. is_relation 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. R a subset of S x S if and only if is_relation (S,R). equivalence_closure 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. transitive_closure 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. reflexive_closure 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. symmetric_closure 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. is_transitive This symbol represents the boolean binary function which returns true if and only if the second argument is a transitive relation on the first. 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. is_reflexive This symbol represents the boolean binary function which returns true if and only if the second argument is a reflexive relation on the first. is_reflexive(S,R) if and only if, for all, a in S, we have (a,a) in R. is_symmetric This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first. 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. is_equivalence This symbol represents the boolean binary function which returns true if and only if the second argument is a symmetric relation on the first. R is an equivalence relation on S if and only if R is a symmetric, reflexive, transitive relation on S. class 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}. class(S,R,a) = {b in S | (a,b) in R}. classes 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. The classes of an equivalence relation R on S partition S. The classes of a reflexive relation R on S cover S, as a in S belongs to class(S,R,a).