| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 570 B |
|
Impressum continuity_ms_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Continuity definition file % % Author: David Lester, Manchester University & NIA % Rick Butler, NASA Langley % % Version 1.0 5/12/04 Initial Version %------------------------------------------------------------------------------ continuity_ms_def[T1:Type+,d1:[T1,T1->nnreal], T2:Type+,d2:[T2,T2->nnreal]]: THEORY BEGIN ASSUMING IMPORTING metric_spaces_def fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1]) fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2]) ENDASSUMING IMPORTING metric_spaces E: VAR set[T1] epsilon, delta: VAR posreal continuous_at?(f:[T1->T2], E: set[T1],x: (E)):bool = FORALL epsilon: EXISTS delta: FORALL (y:(E)): member(y, ball[T1,d1](x,delta)) IMPLIES member(f(y), ball[T2,d2](f(x),epsilon)) continuous_at?(f:[T1->T2],x:T1):bool = continuous_at?(f,fullset[T1],x) continuous?(f:[T1->T2], E: set[T1]): bool = FORALL (x:(E)): continuous_at?(f,E,x) continuous?(f:[T1->T2]): bool = continuous?(f,fullset[T1]) END continuity_ms_def ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
