Quellcode-Bibliothek composition_continuous.pvs

composition_continuous [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Composition of continuous functions   
%
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING continuous_functions, reals@real_fun_props

  f : VAR [T1 -> T2]
  g : VAR [T2 -> real]
  x0 : VAR T1

  F : VAR { E : setof[real] | subset?(E, T1_pred) }  

  composition_cont     : LEMMA continuous?(f, x0) AND continuous?(g, f(x0))
                           IMPLIES continuous?(g o f, x0)

  composition_cont_set : AXIOM continuous_on?(f, F) AND continuous_on?(g, Im(f, F))
                           IMPLIES continuous_on?(g o f, F)

  composition_cont_fun : LEMMA continuous?(f) AND continuous?(g) 
                                  IMPLIES continuous?(g o f)

END composition_continuous