Quelle  deriv_cont_2D.pvs   Sprache: PVS

deriv_cont_2D [T: TYPE from real]: THEORY
BEGIN 

  ASSUMING
      IMPORTING analysis@deriv_domain_def

      deriv_domain     : ASSUMPTION deriv_domain?[T]

      not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING


  IMPORTING cont_real_vect2, deriv_real_vect2, analysis@derivatives

  v,u : VAR Vect2
  x,y : VAR real
  nzx : VAR nzreal

  f: VAR [T -> Vect2]


  derivable_rv_cont_rv: LEMMA derivable_rv?(f) IMPLIES continuous_rv?(f)


END deriv_cont_2D