Library ▹ Essentials ▹ Functions
Definition 1.5.7.  Let X be a set. We define:
idX :  X → Xx ↦ 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
[View Source]