counting the number of idempotent relations has been derived in Isabelle/HOL. 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 for some . This is used to show that certain subspaces of an uncountable product of spaces, known as Mahavier products, cannot be metrizable when defined by a nontrivial idempotent relation. References Further reading Binary relations