Idempotent relation
In mathematics, an idempotent binary relation R ⊆ X × X is one for which R ∘ R = R.[1][2] This notion generalizes that of an idempotent function to relations. Each idempotent relation is necessarily transitive, as the latter means R ∘ R ⊆ R.
For example, the relation < on ℚ is idempotent. In contrast, < on ℤ is not, since (<) ∘ (<) ⊇ (<) does not hold: e.g. 1 < 2, but 1 < x < 2 is false for every x ∈ ℤ.
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. [3][4]
References
- Lua error in package.lua at line 80: module 'strict' not found.
<templatestyles src="Asbox/styles.css"></templatestyles>
 |
This mathematics-related article is a stub. You can help Wikipedia by expanding it. |
