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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: ml_print_depth0.ML   Sprache: PVS

Original von: PVS©
%------------------------------------------------------------------------------
% Product of Complete Metric Spaces
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            20/12/07  Initial Version
%------------------------------------------------------------------------------

complete_product[T0,T1:TYPE, (IMPORTING metric_def)
                 d0:metric[T0],d1:metric[T1]]: THEORY

BEGIN

  z0,z1: VAR [T0,T1]

  IMPORTING reals@sqrt,
            metric_space_def[T0,d0],
            metric_space_def[T1,d1],
            metric_space_def,
            metric_def

  d2: MACRO metric[[T0,T1]] =
       (LAMBDA (z0,z1): sqrt(sq(d0(z0`1,z1`1))+sq(d1(z0`2,z1`2))))

  complete_d2: LEMMA metric_complete?(fullset[T0]) AND
                     metric_complete?(fullset[T1]) =>
                     metric_complete?[[T0,T1],d2](fullset[[T0,T1]])

END complete_product

¤ Dauer der Verarbeitung: 0.13 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff