|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
