%-------------------------------------------------------------------------
%
% Infinite images of a set under some function.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: infinite_sets_def[D], infinite_sets_def[R]
% sets_aux: infinite_image[D,R]
%
%-------------------------------------------------------------------------
infinite_image[D: TYPE, R: TYPE]: THEORY
BEGIN
IMPORTING infinite_sets_def[D], infinite_sets_def[R]
infinite_image: THEOREM
FORALL (S: set[D]), (f: [D -> R]):
is_infinite[R](image(f, S)) => is_infinite[D](S)
f: VAR (injective?[D, R])
S: VAR infinite_set[D]
infinite_injective_image: JUDGEMENT image(f, S) HAS_TYPE infinite_set[R]
END infinite_image
¤ Dauer der Verarbeitung: 0.13 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.
|
