Library
▹
Essentials
▹
Relations
Definition 1.4.8.
Let
S
be a set. We define:
(=
S
)
:
=
[
s
=
t
]
s
,
t
∈
S
References.
https://en.wikipedia.org/wiki/Binary_relation#Particular_binary_relations
: identity relation
https://proofwiki.org/wiki/Definition:Diagonal_Relation
https://leanprover-community.github.io/mathlib_docs/init/core.html#eq