cont_vect[n,m:posnat] : THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vector[n] -> Vector[m] ]   
%
%  Author: Cesar Munoz
%          Ricky Butler     
%          NASA Langley Research Center  8/12/2009
%------------------------------------------------------------------------------
BEGIN

  IMPORTING vectors@vectors

  IMPORTING limit_vect[n,m]

  f, f1, f2,g    : VAR [Vector[n] -> Vector[m]]
  u              : VAR Vector[m]
  x, x0          : VAR Vector[n]
  epsilon, delta : VAR posreal
 
  %--------------------
  %  Continuity at x0    
  %--------------------

  continuous_vv?(f, x0) : bool = 
 FORALL epsilon : EXISTS delta : 
     FORALL x: norm(x-x0) < delta        
                 IMPLIES norm(f(x) - f(x0)) < epsilon

  continuity_def : LEMMA
        continuous_vv?(f, x0) IFF convergence(f, x0, f(x0))

  continuity_def2 : LEMMA
        continuous_vv?(f, x0) IFF convergent?(f, x0)


 %------------------------------------------
 %  Operations preserving continuity at x0 
 %------------------------------------------

  sum_continuous_vv  : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 + f2, x0)

  diff_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 - f2, x0)

  const_continuous_vv: LEMMA continuous_vv?(const_fun(u), x0)

%%  identity_continuous_vv: LEMMA continuous_vv?((LAMBDA(x):x),x0)

  neg_continuous_vv  : LEMMA continuous_vv?(f, x0) IMPLIES continuous_vv?(- f, x0)

 %---------------------------------
 %  Continuity of f in its domain
 %---------------------------------

  continuous_vv?(f): bool = FORALL x0: continuous_vv?(f, x0)


 %--- Properties ---%

  continuous_vv_fun: TYPE+ = { f | continuous_vv?(f) }

  nz_continuous_vv_fun: TYPE = { g | continuous_vv?(g) }

  h, h1, h2: VAR continuous_vv_fun
  h3: VAR nz_continuous_vv_fun

  sum_fun_continuous_vv : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vv_fun

  diff_fun_continuous_vv: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vv_fun

  const_fun_continuous_vv: JUDGEMENT const_fun(u) HAS_TYPE continuous_vv_fun

  neg_fun_continuous_vv : JUDGEMENT -(h) HAS_TYPE continuous_vv_fun


 % ------------ Alternate forms and names for convenience ---------------

  sum_cont_fun  : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 + f2)

  diff_cont_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 - f2)

  const_cont_fun: LEMMA continuous_vv?(const_fun(u))

  neg_cont_fun  : LEMMA continuous_vv?(f) IMPLIES continuous_vv?(-f)

%%  id_cont_fun   : LEMMA continuous_vv?((LAMBDA(x):x))

END cont_vect