Library
▹
Essentials
▹
Relations
Definition 1.4.12.
Let
S
be a set,
⪯
be a
relation
on
S
. We define:
⪯
is antisymmetric
:
⇔
∀
s
,
t
∈
S
s.t.
s
⪯
t
and
t
⪯
s
:
s
=
t
References.
https://en.wikipedia.org/wiki/Antisymmetric_relation
https://mathworld.wolfram.com/AntisymmetricRelation.html
https://proofwiki.org/wiki/Definition:Antisymmetric_Relation
https://ncatlab.org/nlab/show/antisymmetric+relation
https://coq.inria.fr/library/Coq.Sets.Relations_1.html#Antisymmetric
https://leanprover-community.github.io/mathlib_docs/init/logic.html#anti_symmetric