Quelle  countable_cross.pvs

%------------------------------------------------------------------------------
% Countable cross products
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            17/08/07  Initial Version
%------------------------------------------------------------------------------
countable_cross[T1,T2:TYPE]: THEORY

BEGIN


  IMPORTING sets_aux@countability,
            topology@cross_product[T1,T2]

  X: VAR set[T1]
  Y: VAR set[T2]

  is_countable_cross: LEMMA is_countable(X) AND is_countable(Y) =>
                            is_countable(cross_product(X,Y))

END countable_cross