Go up to 6 More on FunctionsGo forward to 6.2 Counting Set Elements |

Thef(A') :=ifA' subset domain(f)then{f(x):xinA'}.

f^{-1}(B') := {xin domain(f):f(x) inB'}.

The set `f`(`A`') is visualized in the following figure
(where `f`^{-1}(`f`(`A`')) = `A`'):

**Logic Evaluator**
The corresponding definitions are as follows:

Next we define a particular classification of functions.

f:A->^{injective}B: <=>f:A->B/\ (forallx_{0}inA,x_{1}inA:f(x_{0}) =f(x_{1}) =>x_{0}=x_{1}).

f:A->^{surjective}B: <=>f:A->B/\ (forallyinB:existsxinA:f(x) =y).

f:A->^{bijective}B: <=>f:A->^{injective}B/\f:A->^{surjective}B.

These new notions are visualized in the following figure:

For an injective function, the image of the function domain is at least as large as the domain; for a surjective function, the domain is at least as large as the image. If a function is injective and surjective, the domain and its image thus have the same size.

- The
*identity function (Identität)*`f`(`x`):=`x`is*bijective*because it intersects every horizontal line exactly once: - The
*square function (Quadratfunktion)*`f`(`x`):=`x`^{2}is*neither*injective (because the horizontal lines with positive vertical coordinates are intersected twice)*nor*surjective (because the horizontal lines with negative coordinates are not intersected at all). - The function
`f`(`x`):=`x`^{3}-`x`is*surjective*but not injective (every horizontal line is intersected at least once, some horizontal lines are intersected more than once):

**Logic Evaluator**
The new predicates are defined below.

Bijectivity is preserved by function composition.

forallA,B,C,f:A->^{bijective}B,g:B->^{bijective}C:fog:A->^{bijective}C.

- We show
`f`o`g`is injective. Take arbitrary`x`_{0}in`A`and`x`_{1}in`A`with (`f`o`g`)(`x`_{0}) = (`f`o`g`)(`x`_{1}). We have to show`x`_{0}=`x`_{1}.We know, by definition of o , that

`g`(`f`(`x`_{0})) =`g`(`f`(`x`_{1})) and thus, because`g`is injective,`f`(`x`_{0}) =`f`(`x`_{1}). Since`f`is injective, we then have`x`_{0}=`x`_{1}. - We show
`f`o`g`is surjective. Take arbitrary`z`in`C`; we have to find some`x`such that (`f`o`g`)(`x`) =`z`.Since

`g`is surjective, we have some`y`in`B`such that`g`(`y`) =`z`. Since`f`is surjective, we have some`x`in`A`such that`f`(`x`) =`y`. Thus (`f`o`g`)(`x`) =`g`(`f`(`x`)) =`g`(`y`) =`z`.

As we have seen in Section *Functions as Sets*, the inverse of a
function is not necessarily a function. However, we have the following result.

forallA,B,f:A->^{injective}B:f^{-1}:B->A.

By Proposition *Inverse of a Relation*, we have `f`^{-1} subset `B` x `A`. By Definition *Function*, it remains to be shown

(Take arbitraryforallx,y_{0},y_{1}: (<x,y_{0}> inf^{-1}/\ <x,y_{1}> inf^{-1}) =>y_{0}=y_{1}).

(1) <We have to show (2)x,y_{0}> inf^{-1}/\ <x,y_{1}> inf^{-1}.

From (1) and Definition *Inverse*, we know

(3) <i.e.,y_{0},x> inf/\ <y_{1},x> inf,

**Logic Evaluator**
The fact that the inverse of an injective function is also a function is
demonstrated below at the example of negation on **Z**(which is injective) and
of the absolute value (which is not injective) using the definitions in file
`function.txt`

.

The following function is the result of the composition of a function with its inverse.

1 _{A}:A->A1 _{A}(x) :=x

If

fo 1_{B}= f1 _{A}of= f.

If

fof^{-1}= 1 _{A}

f^{-1}of= 1 _{B}.

We can consider the set of all functions over some set `A` as a domain
with a binary operation o (which is associative), a unary operation
^{-1} (the inverse) and a neutral element 1_{A}.

**Logic Evaluator**
We demonstrate the properties of the identity function listed above.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999