|
%------------------------------------------------------------------------------
% Enumerations of finite sets
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
finite_enumeration[T:TYPE]: THEORY
BEGIN
finite_enumeration(X:finite_set[T]): [below[card(X)]->(X)]
= choose({f:[below[card(X)]->(X)] | bijective?[below[card(X)],(X)](f)})
X: VAR finite_set[T]
finite_enumeration_bij: LEMMA
bijective?[below[card(X)],(X)](finite_enumeration(X))
finite_enumeration_image: LEMMA
image(finite_enumeration(X),fullset[below[card(X)]]) = X
END finite_enumeration
¤ Dauer der Verarbeitung: 0.2 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.
|
