relation0 http://www.openmath.org/cd/relation0.ocd 2003-04-01 experimental 1999-06-01 1 1 Binary relations properties, equivalence relation, orders, up to the definition of a setoid as a set with an equivalence relations defined on its elements. Initial version: O. Caprotti relation Type constructor; returns the type of binary relations on a set. Is defined as "[A:Set] A -> A -> Prop" reflexive Proposition; the type of reflexive binary relations. Defined as [A:symtype][R: (relation A)](x:A)(R x x) irreflexive Proposition; the type of irreflexive binary relations. Defined as [A:symtype][R: (relation A)](x:A) ~(R x x) transitive Proposition; the type of transitive binary relations. Defined as [A:symtype][R: (relation A)](x,y,z:A)(R x y) -> (R y z) -> (R x z) symmetric Proposition; the type of symmetric binary relations. Defined as [A:symtype][R: (relation A)](x,y:A)(R x y) -> (R y x) antisymmetric Proposition; the type of antisymmetric binary relations. Defined as [A:symtype][R: (relation A)](x,y:A)(R x y) -> (R y x) -> (relation1::eq x y) partial_equivalence Proposition; the type of partial_equivalence relations, namely relations that are symmetric, and transitive. Defined as [A:symtype][R: (relation A)] (symmetric R) /\ (transitive R) equivalence Proposition; the type of equivalence relations, namely relations that are reflexive, symmetric and transitive. Defined as [A:symtype][R: (relation A)] (reflexive R) /\ (symmetric R) /\ (transitive R) order Proposition; the type of order relations, namely relations that are reflexive, antisymmetric and transitive. Defined as [A:symtype][R: (relation A)] (reflexive R) /\ (antisymmetric R) /\ (transitive R) strict_order Proposition; the type of strict order relations, namely relations that are irreflexive, antisymmetric and transitive. Defined as [A:symtype][R: (relation A)] (irreflexive R) /\ (antisymmetric R) /\ (transitive R) pre_order Proposition; the type of preorder relations, namely relations that are reflexive and transitive. Defined as [A:symtype][R: (relation A)] (reflexive R) /\ (transitive R)