Library
▹
Essentials
▹
Functions
Definition 1.5.7.
Let
X
be a set. We define:
id
X
:
X
→
X
x
↦
x
References.
https://en.wikipedia.org/wiki/Identity_function
https://proofwiki.org/wiki/Definition:Identity_Mapping
https://coq.inria.fr/library/Coq.Init.Datatypes.html#id
https://leanprover-community.github.io/mathlib_docs/init/logic.html#id