Quelle  countable_image.pvs

%------------------------------------------------------------------------------
% image of a countable set is countable
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            2/1/05
%------------------------------------------------------------------------------

countable_image[D,R:TYPE]: THEORY
BEGIN

  f: VAR [D->R]
  S: VAR set[D]

  IMPORTING countability,
            function_image_aux[D,R],
            infinite_image,
            card_function[D,R]

  countable_image: THEOREM is_countable(S) => is_countable(image(f)(S))

END countable_image