===== Inverse function =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $ f\in X^Y_\text{inj} $ |

| @#55EE55: postulate   | @#55EE55: $ f^{-1} \equiv f^\smile $ |

==== Discussion ====
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 function]]s 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: [[http://mizar.org/JFM/Vol1/funct_1.html|FUNCT_1]]

==== Parents ====
=== Context ===
[[Injective function]], [[Reversed relation]]