|
%------------------------------------------------------------------------------
% Enumerations of countably infinite sets
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
denumerable_enumeration[T:TYPE]: THEORY
BEGIN
IMPORTING sets_aux@countable_props[T]
denumerable_enumeration(X:countably_infinite_set[T]): [nat->(X)]
= choose({f:[nat->(X)] | bijective?[nat,(X)](f)})
X: VAR countably_infinite_set[T]
denumerable_enumeration_bij: LEMMA
bijective?[nat,(X)](denumerable_enumeration(X))
denumerable_enumeration_image: LEMMA
image(denumerable_enumeration(X),fullset[nat]) = X
END denumerable_enumeration
¤ Dauer der Verarbeitung: 0.0 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.
|
