Go backward to C.7 Complex NumbersGo up to C Logic Evaluator DefinitionsGo forward to C.9 Real Functions

C.8 More on Functions

```// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// functions
//
// (c) 1999, Wolfgang Schreiner, see file COPYRIGHT
// http://www.risc.uni-linz.ac.at/software/formal
// ----------------------------------------------------------------

// the image of A' at f
fun image(f: Function, A': Set) =
if(isSubset(A', domain(f)), set(x in A': true, apply(f, x)));

// the inverse image of B' at f
fun image^-1(f: Function, B': Set) =
set(x in domain(f): in(apply(f, x), B'), x);

// f is injective from A to B
pred isInjective(f: Function, A: Set, B: Set) <=>
and(isFunction(f, A, B),
forall(x0 in A, x1 in A:
implies(=(apply(f, x0), apply(f, x1)), =(x0, x1))));

// f is surjective from A to B
pred isSurjective(f: Function, A: Set, B: Set) <=>
and(isFunction(f, A, B),
forall(y in B:
exists(x in A: =(apply(f, x), y))));

// f is bijective between A and B
pred isBijective(f: Function, A: Set, B: Set) <=>
and(isInjective(f, A, B), isSurjective(f, A, B));

// ----------------------------------------------------------------
// \$Id: evaluator.tex,v 1.7 1999/09/29 12:28:26 schreine Exp \$
// ----------------------------------------------------------------
```

Author: Wolfgang Schreiner
Last Modification: October 4, 1999