|
% to be added to Jerry James's function_image_aux theory in the prelude
function_image_nonempty[D: TYPE, R: TYPE]: THEORY
BEGIN
f: VAR [D -> R]
S: VAR set[D]
nonempty_image: JUDGEMENT
image(f, (S: (nonempty?[D]))) HAS_TYPE (nonempty?[R])
nonempty_finite_image: JUDGEMENT
image(f, (S: non_empty_finite_set[D])) HAS_TYPE non_empty_finite_set[R]
% image_witness: JUDGEMENT
% f(x: (S)) HAS_TYPE (image?(f, S))
END function_image_nonempty
¤ Dauer der Verarbeitung: 0.17 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.
|
