Go up to 6 More on Functions Go forward to 6.2 Counting Set Elements |
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.
f is surjective (surjektiv) (also called onto) if it every element of B is hit by some argument:
f: A ->injective B : <=> f: A -> B /\ (forall x0 in A, x1 in A: f(x0) = f(x1) => x0 = x1).
f is bijective (bijektiv) if it is injective and surjective:
f: A ->surjective B : <=> f: A -> B /\ (forall y in B: exists x in A: 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.
Logic Evaluator The new predicates are defined below.
Bijectivity is preserved by function composition.
forall A, B, C, f: A ->bijective B, g: B ->bijective C: f o g: A ->bijective C.
We know, by definition of o , that g(f(x0)) = g(f(x1)) and thus, because g is injective, f(x0) = f(x1). Since f is injective, we then have x0 = x1.
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.
forall A, 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
(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.
1A: A -> A 1A(x) := x
If f is injective, then we have
f o 1B = f 1A o f = f.
If f is also surjective (i.e., bijective), then we have
f o f-1 = 1A
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.