vect_vect_2D_continuity: THEORY

%%% A theory of continuity for functions from [Vect2,Nz_vect2] into
%%% both Vect2 and real

BEGIN

  IMPORTING vectors@vectors_2D

  ffv,ggv,hhv : VAR [[Vect2,Nz_vect2]->Vect2]
  ffr,ggr,hhr : VAR [[Vect2,Nz_vect2]->real]
  s       : VAR Vect2
  nzv       : VAR Nz_vect2
  c       : VAR real

  continuous_vvv?(ffv): bool =
    FORALL (epsil:posreal,s:Vect2,nzv:Nz_vect2): 
    EXISTS (ds, dv: posreal):
    FORALL (sp:Vect2,nzvp:Nz_vect2):
         norm(s - sp) < ds AND
         norm(nzv-nzvp) < dv
         IMPLIES
         norm(ffv(s, nzv) - ffv(sp,nzvp)) < epsil

  sum_vvv(ggv,hhv)(s,nzv): Vect2 = ggv(s,nzv)+hhv(s,nzv)

  diff_vvv(ggv,hhv)(s,nzv): Vect2 = ggv(s,nzv)-hhv(s,nzv)

  scal_vvv(c,hhv)(s,nzv): Vect2 = c*hhv(s,nzv)

  continuous_vvr?(ffr): bool =
    FORALL (epsil:posreal,s:Vect2,nzv:Nz_vect2): 
    EXISTS (ds, dv: posreal):
    FORALL (sp:Vect2,nzvp:Nz_vect2):
         norm(s - sp) < ds AND
         norm(nzv-nzvp) < dv
         IMPLIES
         abs(ffr(s, nzv) - ffr(sp,nzvp)) < epsil

  sum_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)+hhr(s,nzv)

  diff_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)-hhr(s,nzv)

  prod_vvr(ggr,hhr)(s,nzv): real = ggr(s,nzv)*hhr(s,nzv)

  max_vvr(ggr,hhr)(s,nzv): real = max(ggr(s,nzv),hhr(s,nzv))

  scal_vvr(c,hhr)(s,nzv): real = c*hhr(s,nzv)

  const_vvr(c)(s,nzv): real = c

  scal_vvr_vvv(ffr,ggv)(s,nzv): Vect2 = ffr(s,nzv)*ggv(s,nzv)

  dot_vvv(ffv,ggv)(s,nzv): real = ffv(s,nzv)*ggv(s,nzv)

  nzero_vvr?(ffr): bool = (FORALL (s,nzv): ffr(s,nzv)/=0)

  continuous_nz_vvr?(ffr): bool = continuous_vvr?(ffr) AND nzero_vvr?(ffr)

  ffvc,ggvc,hhvc: VAR (continuous_vvv?)
  ffrc,ggrc,hhrc: VAR (continuous_vvr?)
  ggnz  : VAR (nzero_vvr?)
  ggnzc  : VAR (continuous_nz_vvr?)

  div_vvr(ffr,ggnz)(s,nzv): real = ffr(s,nzv)/ggnz(s,nzv)

  norm_vvv(ffv)(s,nzv): nnreal = norm(ffv(s,nzv))



  %%%%%%%           %%%%%%%

  sum_vvv_cont: LEMMA continuous_vvv?(sum_vvv(ffvc,ggvc))

  sum_vvr_cont: LEMMA continuous_vvr?(sum_vvr(ffrc,ggrc))

  diff_vvv_cont: LEMMA continuous_vvv?(diff_vvv(ffvc,ggvc))

  scal_vvv_cont: LEMMA continuous_vvv?(scal_vvv(c,ffvc))
  
  dot_vvv_cont: LEMMA continuous_vvr?(dot_vvv(ffvc,ggvc))

  prod_vvr_cont: LEMMA continuous_vvr?(prod_vvr(ffrc,ggrc))

  const_vvr_cont: LEMMA continuous_vvr?(const_vvr(c))

  scal_vvr_vvv_cont: LEMMA continuous_vvv?(scal_vvr_vvv(ffrc,ggvc))

  scal_vvr_cont: LEMMA continuous_vvr?(scal_vvr(c,ffrc))

  div_vvr_cont: LEMMA continuous_vvr?(div_vvr(ffrc,ggnzc))

  nzv_vvv_cont: LEMMA continuous_vvv?(LAMBDA (s,nzv): nzv)

  s_vvv_cont: LEMMA continuous_vvv?(LAMBDA (s,nzv): s)

  max_vvr_cont: LEMMA continuous_vvr?(max_vvr(ffrc,ggrc))

  norm_vvv_cont: LEMMA continuous_vvr?(norm_vvv(ffvc))




END vect_vect_2D_continuity