Library ▹ Essentials ▹ Relations
Definition 1.4.15.  Let S be a set, ⪯ be a relation on S. We define:
⪯ is a partial order  :⇔  ⪯ is reflexive and ⪯ is antisymmetric and ⪯ is transitive  ⇔  ⪯ is a preorder and ⪯ is antisymmetric
Equivalence.  No proof.
References.
  • https://en.wikipedia.org/wiki/Partially_ordered_set#Formal_definition
  • https://mathworld.wolfram.com/PartialOrder.html
  • https://proofwiki.org/wiki/Definition:Ordering
  • https://coq.inria.fr/library/Coq.Sets.Relations_1.html#Order
  • https://leanprover-community.github.io/mathlib_docs/init/algebra/order.html#partial_order
[View Source]