% Additions to standard prelude theory function_image
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06

function_image_bis[D,R:TYPE]: THEORY

BEGIN

  IMPORTING function_image[D,R]

  f:    VAR [D->R]
  X:    VAR set[D]
  Y:    VAR set[R]
  inj:  VAR (injective?[D,R])
  surj: VAR (surjective?[D,R])
  bij:  VAR (bijective?[D,R])

  image_emptyset: LEMMA image(f,emptyset[D]) = emptyset[R]

  inverse_image_emptyset: LEMMA inverse_image(f,emptyset[R]) = emptyset[D]

  surjective_image_inverse_image: LEMMA image(surj,inverse_image(surj,Y)) = Y

  injective_inverse_image_image:  LEMMA inverse_image(inj,image(inj,X))   = X

  bijective_image_iff_inverse_image: LEMMA
     image(bij,X) = Y IFF inverse_image(bij,Y) = X

% I'm not sure that this last item belongs in this particular library.

  bijective_image_inverse_alt: LEMMA FORALL (bij:(bijective?[D,R])):
     inverse_image(bij,Y) = IF empty?(Y) THEN emptyset[D]
                            ELSE image(inverse_alt(bij),Y) ENDIF

END function_image_bis