Go backward to C.7 Complex Numbers Go up to C Logic Evaluator Definitions Go 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
// ----------------------------------------------------------------

read relation;

// 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 $
// ----------------------------------------------------------------