%--------------------------------------------------------------------------------------------------
%
% Product (Metric) Spaces
%
% Author: Anthony Narkawicz, NASA Langley
%
%
% Version 1.0 August 19, 2009
%
%--------------------------------------------------------------------------------------------------


cross_metric_spaces[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 metric_spaces, reals@sqrt,reals@sq

  X,S: VAR set[T1]
  Y,T: VAR set[T2]
  x,y: VAR [T1,T2]
  z,w: VAR T2

 
  d(x,y): nnreal = d1(x`1,y`1) + d2(x`2,y`2)

  product_is_metric:  LEMMA metric_space?[[T1,T2],d](fullset[[T1,T2]])

  d_square(x,y): nnreal = sqrt(sq(d1(x`1,y`1)) + sq(d2(x`2,y`2)))

  product_is_metric_square: LEMMA metric_space?[[T1,T2],d_square](fullset[[T1,T2]])


  %% These to metrics produce equivalent topologies %%

  V,U: VAR set[[T1,T2]]

  % a quick lemma that will be used in the proof of the metric equivalence...

  euclic_linear_lemma: LEMMA   
     FORALL (a,b,r: nnreal): sqrt(sq(a) + sq(b)) < r/2 implies a+b<r

  metric_equivalence:  LEMMA   
     open_in?[[T1,T2],d](V,U) IFF open_in?[[T1,T2],d_square](V,U)

  metric_equivalence2: COROLLARY 
     open?[[T1,T2],d](V) IFF open?[[T1,T2],d_square](V)

END cross_metric_spaces