products/Sources/formale Sprachen/PVS/sigma_set/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: riesz_linear_functionals.prf   Sprache: Unknown

%------------------------------------------------------------------------------
% 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.16 Sekunden  (vorverarbeitet)  ]