SSL infinite_image.pvs

%-------------------------------------------------------------------------
%
%  Infinite images of a set under some function.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: infinite_sets_def[D], infinite_sets_def[R]
%  sets_aux: infinite_image[D,R]
%
%-------------------------------------------------------------------------
infinite_image[D: TYPE, R: TYPE]: THEORY
 BEGIN

  IMPORTING infinite_sets_def[D], infinite_sets_def[R]

  infinite_image: THEOREM
    FORALL (S: set[D]), (f: [D -> R]):
      is_infinite[R](image(f, S)) => is_infinite[D](S)

  f: VAR (injective?[D, R])
  S: VAR infinite_set[D]

  infinite_injective_image: JUDGEMENT image(f, S) HAS_TYPE infinite_set[R]

 END infinite_image