Library ▹ Essentials ▹ Relations
Definition 1.4.14.  Let S be a set, ⪯ be a relation on S. We define:
⪯ is a preorder  :⇔  ⪯ is reflexive and ⪯ is transitive
References.
  • https://en.wikipedia.org/wiki/Preorder
  • https://mathworld.wolfram.com/Preorder.html
  • https://proofwiki.org/wiki/Definition:Preordering
  • https://ncatlab.org/nlab/show/preorder
  • https://coq.inria.fr/library/Coq.Sets.Relations_1.html#Preorder
  • https://leanprover-community.github.io/mathlib_docs/init/algebra/order.html#preorder
[View Source]