Library
▹
Essentials
▹
Relations
Definition 1.4.3.
Let
S
,
T
be sets,
≺
be a
relation
from
S
to
T
. We define:
≺
T
:
=
[
s
≺
t
]
t
∈
T
,
s
∈
S
References.
https://en.wikipedia.org/wiki/Converse_relation
https://proofwiki.org/wiki/Definition:Inverse_Relation
https://leanprover-community.github.io/mathlib_docs/data/rel.html#rel.inv