products/Sources/formale Sprachen/Coq/checker/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: cayleys.prf   Sprache: Unknown

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

[ Dauer der Verarbeitung: 0.32 Sekunden  (vorverarbeitet)  ]