metric_space_real_fun[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% This Theory Contains Standard Lemmas About Real-Valued Continuous Functions
%             On An Arbitrary Metric Space
%
%     Authors: Anthony Narkawicz,  NASA Langley
%
%     Version 1.0         8/31/2009  Initial Version
%------------------------------------------------------------------------------
BEGIN

   ASSUMING IMPORTING metric_spaces_def[T,d]
       fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
   ENDASSUMING

   S: VAR set[T]


   IMPORTING real_metric_space, continuity_ms_def[T,d,real,real_dist], reals@abs_lems

   f,g: VAR [T -> real]
   c: VAR real

   scal_continuous: LEMMA continuous?(f,S) IMPLIES continuous?(c* f, S)
   neg_continuous:  LEMMA continuous?(f,S) IMPLIES continuous?( -f,S)
   sum_continuous:  LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
            continuous?(f+g,S)
   diff_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
            continuous?(f-g,S)
   prod_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
            continuous?(f*g,S)
   abs_comp_cont:  LEMMA continuous?(f,S) IMPLIES continuous?(abs(f),S)
   

END metric_space_real_fun