previous up next
Go up to 6 More on Functions
Go forward to 6.2 Counting Set Elements
RISC-Linz logo

6.1 Further Notions

We start by introducing some additional notions that help to describe the "shape" of functions.

Definition 70 (Image) Let f: A -> B, A' subset A. The  image (Bild) of A' at f is the set of all values to which elements of A' are mapped by f:
f(A') := if A' subset domain(f) then {f(x): x in A'}.
The  inverse image (Urbild) of B' at f is the set of all elements that are mapped to some elements of B' by f:
f-1(B') := {x in domain(f): f(x) in B'}.

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.

Definition 71 (Function Properties) Let f: A -> B. f is  injective (injektiv) (also called  one-to-one) if it does not map different arguments to the same result:
f: A ->injective B : <=>
   f: A -> B /\  (forall x0 in A, x1 in A: f(x0) = f(x1) => x0 = x1).
f is  surjective (surjektiv) (also called  onto) if it every element of B is hit by some argument:
f: A ->surjective B : <=>
   f: A -> B /\  (forall y in B: exists x in A: f(x) = y).
f is  bijective (bijektiv) if it is injective and surjective:
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.

Example  For functions on R, above properties can be demonstrated by considering the number of intersections of the function graph with horizontal lines:

Logic Evaluator  The new predicates are defined below.

Bijectivity is preserved by function composition.

Proposition 68 (Composition of Bijective Functions) The composition of two bijective functions is also bijective:
forall A, B, C, f: A ->bijective B, g: B ->bijective C:
   f o g: A ->bijective C.

Proof  Take arbitrary f: A ->bijective B, g: B ->bijective C.

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.

Proposition 70 (Inverse of a Function) If a function is injective, its inverse is also a function:
forall A, B, f: A ->injective B:
   f-1: B -> A.

Proof  Take arbitrary f: A ->injective B. We have to show 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

(forall x,y0, y1: (<x, y0> in f-1 /\  <x, y1> in f-1) => y0=y1).
Take arbitrary x, y0, and y1 and assume
(1) <x, y0> in f-1 /\  <x, y1> in f-1.
We have to show (2) y0=y1.

From (1) and Definition Inverse, we know

(3) <y0, x> in f /\  <y1, x> in f,
i.e., f(y0) = x and f(y1) = x. Since f is injective, we thus know (2).

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.

Definition 72 (Identity Function)  1A is the function that maps every x in A to itself:
1A: A -> A
1A(x) := x

Proposition 72 (Inverse Function Properties) For every A, B, f: A -> B, we have
f o 1B = f
1A o f = f.
If f is injective, then we have
f o f-1 = 1A
If f is also surjective (i.e., bijective), then we have
f-1 o f = 1B.

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 1A.

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

Author: Wolfgang Schreiner
Last Modification: October 4, 1999

previous up next