Differences
This shows you the differences between two versions of the page.
inverse_function [2013/06/25 15:46] nikolaj |
inverse_function [2014/03/21 11:11] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ===== Inverse function ===== | ||
- | ==== Definition ==== | ||
- | | @#88DDEE: $ f\in X^Y_\text{inj} $ | | ||
- | | @#55EE55: $ f^{-1} $ | | ||
- | |||
- | | @#55EE55: $ f^\smile $ | | ||
- | |||
- | ==== Ramifications ==== | ||
- | We have | ||
- | |||
- | $\text{im}(f^{-1})=\text{dom}(f)=X,$ | ||
- | |||
- | $\hspace{1cm} \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]] | ||
- | |||
- | ==== Context ==== | ||
- | Set constructor | ||
- | === Parents === | ||
- | [[Injective function]], [[Reversed relation]] |