|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
