|
permutation[N: nat]: THEORY
%----------------------------------------------------------------------------
% the theory of bijective mappings from below(N) to below(N)
%
% Author: Alfons Geser, National Institute of Aerospace, Hampton, VA, 2003
%----------------------------------------------------------------------------
BEGIN
permutation: TYPE+ = {pi: [below(N) -> below(N)] | bijective?(pi)}
CONTAINING id
i,j,k : VAR below(N)
m : VAR below(N+1)
pi, rho: VAR permutation
inverse_id : LEMMA N > 0 IMPLIES inverse[below(N),below(N)](id) = id
inverse_composition: LEMMA N > 0 IMPLIES inverse(pi o rho) = inverse(rho) o inverse(pi)
transpose(i,j): permutation =
LAMBDA k: IF k = j THEN i ELSIF k = i THEN j ELSE k ENDIF
involutorian_transpose: LEMMA transpose(i,j)(transpose(i,j)(k)) = k
END permutation
¤ Dauer der Verarbeitung: 0.13 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.
|
