%------------------------------------------------------------------------------ % Generalised constant functions % % Generalises real constant functions. % % Author: David Lester, Manchester University, NIA, Université Perpignan % % Version 1.0 8/10/04 Initial Version % Version 1.0 8/10/04 Generalised (inverse-)image %------------------------------------------------------------------------------
const_fun_def[S,T:TYPE]: THEORY
BEGIN
x: VAR S
a: VAR T
X: VAR set[S]
Y: VAR set[T]
const_fun(a): [S->T] = LAMBDA x : a
constant?(f:[S->T]):bool = EXISTS a: f = const_fun(a)
image_const: LEMMA
image(const_fun(a),X)
= IF empty?(X) THEN emptyset[T] ELSE singleton(a) ENDIF
inverse_image_const: LEMMA
inverse_image(const_fun(a),Y)
= IF Y(a) THEN fullset[S] ELSE emptyset[S] ENDIF
END const_fun_def
¤ 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.0.19Bemerkung:
(vorverarbeitet)
¤
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.
