%---------------------------------------------------------------------------------------------------------
%
%       One-Variable Uniform Continuity of Real Valued Functions on Product Metric Spaces
%
%       Author: Anthony Narkawicz, NASA Langley
%
%       
%       Version 1.0                     August 27, 2009
%
%---------------------------------------------------------------------------------------------------------


cross_metric_real_fun[T1:Type+,d1:[T1,T1->nnreal],
                  T2:Type+,d2:[T2,T2->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])

    ENDASSUMING

  IMPORTING real_metric_space,cross_metric_uniform_continuity[T1,d1,T2,d2,real,real_dist], continuity_ms[T2,d2,real,real_dist], real_fun_on_compact_sets[T1,d1]

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




  % If X is compact, then the function unif_min_first(f,X) = (LAMBDA (t: T2) = min({r: real | EXISTS (x: (X)): r = f(x,t)}))
  % is continuous.

  IMPORTING reals@bounded_reals[real]

  % The main TCC:

  curried_min_exists: LEMMA nonempty?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND compact?(X)
     IMPLIES (FORALL (t: T2): Y(t) IMPLIES
         nonempty?[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
          below_bounded[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
           ext[real]({r: real | EXISTS (x: (X)): r = f(x, t)})(inf[real]({r: real | EXISTS (x: (X)): r = f(x, t)}))
    AND (EXISTS (x: (X)): FORALL (y: (X)): f(x,t) <= f(y,t)))

  curried_min_is_cont: THEOREM (compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND nonempty?(X)) IMPLIES
           LET unif_min_first(t: T2): real = IF Y(t) THEN min({r: real | EXISTS (x: (X)): r = f(x,t)}) ELSE 0 ENDIF
         IN  continuous?(unif_min_first,Y)

  

END cross_metric_real_fun