%---------------------------------------------------------------------------------------------------
%
%       One-Variable Uniform Continuity of Functions on Product (Metric) Spaces
%
%       Author: Anthony Narkawicz, NASA Langley
%
%       
%       Version 1.0                     August 25, 2009
%
%---------------------------------------------------------------------------------------------------


cross_metric_uniform_continuity[T1:Type+,d1:[T1,T1->nnreal],
                  T2:Type+,d2:[T2,T2->nnreal],T3:TYPE+,d3:[T3,T3->nnreal]]: THEORY

BEGIN

    ASSUMING IMPORTING metric_spaces

        fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
        fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])
        fullset_metric_space3: ASSUMPTION metric_space?[T3,d3](fullset[T3])

    ENDASSUMING

  IMPORTING cross_metric_spaces[T1,d1,T2,d2], continuity_ms_def[[T1,T2],d[T1,d1,T2,d2],T3,d3], 
            cross_metric_cont[T1,d1,T2,d2,T3,d3], compactness[T1,d1]

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

  multiary_Heine: THEOREM 
     compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) 
     IMPLIES uniformly_continuous_in_first?(f,X,Y)

  multi_Heine_Corollary1: COROLLARY 
     compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) 
     IMPLIES 
          FORALL (y1: (Y), epsilon: posreal): EXISTS (delta: posreal):
             FORALL (y2: (Y)): (d2(y1,y2) <= delta) 
                IMPLIES (FORALL (x: (X)): d3(f(x,y1),f(x,y2)) < epsilon)


  % A Type Consisting Of All Functions That Are Uniformly Continuous In The First Variable

  first_var_unif(X,Y): TYPE = {g: [[T1,T2] -> T3] | uniformly_continuous_in_first?(g,X,Y)}
  

END cross_metric_uniform_continuity