Inverse function

Set

context $ f\in X^Y_\text{inj} $
postulate $ 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 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

Parents

Context

Injective function, Reversed relation