Library
▹
Essentials
▹
Relations
Definition 1.4.10.
Let
S
be a set,
≺
be a
relation
on
S
. We define:
≺
is connex
:
⇔
∀
s
,
t
∈
S
: [
s
≺
t
or
t
≺
s
]
References.
https://en.wikipedia.org/wiki/Connex_relation
https://proofwiki.org/wiki/Definition:Total_Relation
https://ncatlab.org/nlab/show/total+relation
https://leanprover-community.github.io/mathlib_docs/init/logic.html#total