The strict ordering relation is transitive, and whenever two rational numbers x and z obey the relation x < z there necessarily exists another rational number y between them (for instance, their average) with x < y and y < z.
An outer product of logical vectors forms an idempotent relation.
Idempotent relations have been used as an example to illustrate the application of Mechanized Formalisation of mathematics using the interactive theorem prover Isabelle/HOL.
Besides checking the mathematical properties of finite idempotent relations, an algorithm for counting the number of idempotent relations has been derived in Isabelle/HOL.
[4][5] Idempotent relations defined on weakly countably compact spaces have also been shown to satisfy "condition Γ": that is, every nontrivial idempotent relation on such a space contains points