Quelle  continuity_def.pvs

%------------------------------------------------------------------------------
% Continuity definition file
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            5/12/04  Initial Version
%     Version 1.1            8/6/06   Interface change
%------------------------------------------------------------------------------

continuity_def[T1:Type, (IMPORTING topology_def[T1]) S:topology[T1],
               T2:Type, (IMPORTING topology_def[T2]) T:topology[T2]]: THEORY

BEGIN

  IMPORTING topology[T1,S],
            topology[T2,T]

  f: VAR [T1->T2]
  U: VAR set[T2]
  x: VAR T1

  continuous_at?(f,x):bool
    = FORALL U: neighbourhood?[T2,T](U,f(x)) =>
                neighbourhood?[T1,S](inverse_image(f,U),x)

  tcontinuous_at?(f,x): MACRO bool = continuous_at?(f,x)

  continuous?(f): bool = FORALL x: continuous_at?(f,x)

  tcontinuous?(f): MACRO bool = continuous?(f)

  continuous: TYPE = (continuous?)

END continuity_def