%------------------------------------------------------------------------------
% 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