%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|