|
% Additions to standard prelude theory function_image
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06
function_image_bis[D,R:TYPE]: THEORY
BEGIN
IMPORTING function_image[D,R]
f: VAR [D->R]
X: VAR set[D]
Y: VAR set[R]
inj: VAR (injective?[D,R])
surj: VAR (surjective?[D,R])
bij: VAR (bijective?[D,R])
image_emptyset: LEMMA image(f,emptyset[D]) = emptyset[R]
inverse_image_emptyset: LEMMA inverse_image(f,emptyset[R]) = emptyset[D]
surjective_image_inverse_image: LEMMA image(surj,inverse_image(surj,Y)) = Y
injective_inverse_image_image: LEMMA inverse_image(inj,image(inj,X)) = X
bijective_image_iff_inverse_image: LEMMA
image(bij,X) = Y IFF inverse_image(bij,Y) = X
% I'm not sure that this last item belongs in this particular library.
bijective_image_inverse_alt: LEMMA FORALL (bij:(bijective?[D,R])):
inverse_image(bij,Y) = IF empty?(Y) THEN emptyset[D]
ELSE image(inverse_alt(bij),Y) ENDIF
END function_image_bis
¤ Dauer der Verarbeitung: 0.19 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.
|
