Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Apache/modules/mappers/   (Apache Software Stiftung Version 2.4.65©)  Datei vom 11.0.2007 mit Größe 4 kB image not shown  

Quelle  complex_topology.pvs   Sprache: unbekannt

 
%------------------------------------------------------------------------------
% Complex Topology
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            12/3/10   Initial Version
%------------------------------------------------------------------------------

complex_topology: THEORY

BEGIN

  IMPORTING complex_alt@polar,
            metric_space@metric_space[complex,lambda (x,y:complex): abs(x-y)]

  a,x,y: VAR complex
  r:   VAR posreal
  q:   VAR {x | rational?(Re(x)) & rational?(Im(x))}
  pq:  VAR posrat
  X,A: VAR set[complex]


  IMPORTING metric_space@real_topology % Proof Only

  complex_is_complete: JUDGEMENT fullset[complex] HAS_TYPE
                       metric_complete[complex,lambda x,y: abs(x-y)]

END complex_topology

95%


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