|
%------------------------------------------------------------------------------
% 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.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
