This is an old revision of the document!
Inverse function
Definition
| $ f\in X^Y_\text{inj} $ |
| $ f^{-1} $ |
| $ f^\smile $ |
Ramifications
We have
$\text{im}(f^{-1})=\text{dom}(f)=X,$
$\text{dom}(f^{-1})=\text{im}(f).$
Injectiveness of $f$ implies there is a left “left inverse” of the function: $f^{-1}\circ f=\text{id}$.
Surjectiveness implies there is a “right inverse”, so for bijective functions the above line extens to
$\text{dom}(f^{-1})=\text{im}(f)=Y$
and hence for $f:X\to Y$, we can declare $f^{-1}:Y\to X$.
Reference
Mizar files: FUNCT_1
Context
Set constructor
Parents
