|
% Additions to standard prelude theories function_props, and function_props_alt
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06
function_props_aux[T1,T2,T3:TYPE]: THEORY
BEGIN
f1: VAR [T1->T2]
f2: VAR [T2->T3]
Y: VAR set[T3]
inverse_image_composition: LEMMA
inverse_image(f1, inverse_image(f2,Y)) = inverse_image(f2 o f1, Y)
composition_inverse_alt: LEMMA FORALL (f1:(bijective?[T1,T2]),
f2:(bijective?[T2,T3])):
inverse_alt(f2 o f1)
= inverse_alt(f1) o inverse_alt(f2)
END function_props_aux
¤ Dauer der Verarbeitung: 0.22 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.
|
