Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: modulo_equivalence.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% Continuity over Metric Spaces
%
%     Author: David Lester, Manchester University & NIA
%              Anthony Narkawicz,  NASA Langley
%              Ricky Butler,       NASA Langley
%
%
%     Version 1.0            5/12/04  Initial Version
%------------------------------------------------------------------------------

continuity_ms[T1:Type+,d1:[T1,T1->nnreal],
           T2:Type+,d2:[T2,T2->nnreal]]: THEORY

BEGIN
    ASSUMING IMPORTING metric_spaces

        fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
        fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])

    ENDASSUMING

  IMPORTING continuity_ms_def[T1,d1,T2,d2], compactness[T1,d1]

  X,S: VAR set[T1]
  Y,T: VAR set[T2]

  % Theorem 4.22a

  image_inverse_image: THEOREM FORALL (f:[(S)->(T)]): 
            subset?(X,S) AND subset?(Y,T) AND
                           X = inverse_image(f,Y) IMPLIES subset?(image(f,X),Y)

  % Theorem 4.22b

  inverse_image_image: THEOREM FORALL (f:[(S)->(T)]): 
          subset?(X,S) AND subset?(Y,T) AND
                           Y = image(f,X) IMPLIES subset?(X,inverse_image(f,Y))

  % Theorem 4.23

  continuous_open_sets: THEOREM FORALL (f:[T1->T2]):
    continuous?(f,(S)) IFF
    (Forall Y: open?[T2,d2](Y) IMPLIES open_in?[T1,d1](intersection(inverse_image(f,Y),S),S))

  % Theorem 4.24

  continuous_closed_sets: THEOREM FORALL (f:[T1->T2]):
    continuous?(f,(S)) IFF
    (FORALL Y: closed?[T2,d2](Y) IMPLIES closed_in?[T1,d1](intersection(inverse_image(f,Y),S),S))


END continuity_ms

[ Konzepte0.15Was zu einem Entwurf gehört  Wie die Entwicklung von Software durchgeführt wird  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik