Library
▹
Essentials
▹
Functions
Definition 1.5.29.
Let
X
,
Y
be sets,
f
:
X
↔
Y
be a
bijection
. For
g
:
Y
↔
X
, we define:
f
-1
=
g
:
⇔
g
∘
f
=
id
X
⇔
f
∘
g
=
id
Y
Equivalence.
No proof.
Well-definedness.
No proof.
References.
https://en.wikipedia.org/wiki/Inverse_function
https://mathworld.wolfram.com/InverseFunction.html
https://proofwiki.org/wiki/Definition:Inverse_Mapping
https://ncatlab.org/nlab/show/inverse
https://leanprover-community.github.io/mathlib_docs/logic/function/basic.html#function.inv_fun