products/Sources/formale Sprachen/VDM/VDMPP/PacemakerSeqPP/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: bug_5215_2.v   Sprache: Unknown

%------------------------------------------------------------------------------
% Borel Sets for Hausdorff Spaces
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

hausdorff_borel[T:TYPE, (IMPORTING topology@topology_def[T])
                S:hausdorff]: THEORY

BEGIN

  IMPORTING topology@hausdorff_convergence[T,S],
            borel[T,S]

  x: VAR T

  singleton_is_borel:        LEMMA borel?(singleton(x))

  singleton_is_borel_judge:  JUDGEMENT singleton(x)       HAS_TYPE   borel

END hausdorff_borel

[ zur Elbe Produktseite wechseln0.0Quellennavigators  Analyse erneut starten  ]