Differences

This shows you the differences between two versions of the page.

Link to this comparison view

inverse_function [2013/08/21 11:59]
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} \equiv 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 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]] 
Link to graph
Log In
Improvements of the human condition