%------------------------------------------------------------------------------
% Enumerations of countably infinite sets
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
denumerable_enumeration[T:TYPE]: THEORY

BEGIN

  IMPORTING sets_aux@countable_props[T]

  denumerable_enumeration(X:countably_infinite_set[T]): [nat->(X)]
   = choose({f:[nat->(X)] | bijective?[nat,(X)](f)})

  X: VAR countably_infinite_set[T]

  denumerable_enumeration_bij:   LEMMA
               bijective?[nat,(X)](denumerable_enumeration(X))

  denumerable_enumeration_image: LEMMA
               image(denumerable_enumeration(X),fullset[nat]) = X

END denumerable_enumeration