Quelle  continuity.pvs

%------------------------------------------------------------------------------
% Continuity
%
% All references are to:
%
%   WA Sutherland "Introduction to Metric and Topological Spaces", OUP, 1981
%
% or
%
%   TM Apostol "Mathematical Analysis" 2nd ed, Addison-Wesley, 1974
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            5/12/04  Initial Version
%     Version 1.1            9/6/06   Changed Interface
%------------------------------------------------------------------------------

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

BEGIN

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

  X: VAR set[T1]
  Y: VAR set[T2]
  f: VAR [T1->T2]

  % Apostol Theorem 4.23

  continuous_open_sets: THEOREM
    continuous?(f) IFF
    (FORALL Y: open?[T2,T](Y) => open?[T1,S](inverse_image(f,Y)))

  % Apostol Theorem 4.24

  continuous_closed_sets: THEOREM
    continuous?(f) IFF
    (FORALL Y: closed?[T2,T](Y) => closed?[T1,S](inverse_image(f,Y)))

  B: VAR (base?[T2](T))

  continuous_basis: THEOREM
    continuous?(f) IFF FORALL (Y:(B)): open?[T1,S](inverse_image(f,Y))

END continuity