Quelle  continuity_props.pvs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Properties of continuous functions     %
%  in relation with sequences, limits     %
%  and points of accumulation             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

continuity_props[T : TYPE FROM real] : THEORY

  BEGIN

  IMPORTING continuous_functions, top_sequences

  f : VAR [T -> real]

  u : VAR sequence[T]

  l, a : VAR T


  %--------------------------------------------
  %  u is convergent to l and f is continuous
  %--------------------------------------------

  continuity_limit : LEMMA
 convergence(u, l) AND continuous?(f, l)
      IMPLIES convergence(f o u, f(l))


  %--------------------------------------------
  %  point of accumulation
  %--------------------------------------------

  continuity_accumulation : LEMMA
 accumulation(u, a) AND continuous?(f, a)
     IMPLIES accumulation(f o u, f(a))
  

  END continuity_props