|
% Additions to standard prelude theory function_inverse_alt
%
% David Lester, Manchester University, NIA, Université Perpignan 8/6/06
function_inverse_alt_aux[D,R:TYPE]: THEORY
BEGIN
ASSUMING
inverse_types: ASSUMPTION (EXISTS (d: D): TRUE) OR (FORALL (r: R): FALSE)
ENDASSUMING
f: VAR [D -> R]
inverse_inverse_alt: LEMMA bijective?[D,R](f) =>
inverse_alt(inverse_alt(f)) = f
END function_inverse_alt_aux
¤ Dauer der Verarbeitung: 0.16 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.
|
