Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: continuous_functions_more.pvs Sprache: PVS

Original von: PVS^©

continuous_functions_more [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
%  Additions made by Ricky W. Butler    NASA Langley
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING

     connected_domain : ASSUMPTION
FORALL (x, y : T), (z : real) :
     x <= z AND z <= y IMPLIES T_pred(z)

     not_one_element : ASSUMPTION
  FORALL (x : T) : EXISTS (y : T) : x /= y

   ENDASSUMING

  IMPORTING continuous_functions[T], convergence_sequences

  f: VAR [T -> real]
  a,b,c: VAR T
  cn: VAR sequence[T]
  n: VAR nat

  convergence_fun_of  : LEMMA convergence(cn,c) AND
                               continuous?(f,c) IMPLIES  % move to analysis
                                 convergence(LAMBDA n: f(cn(n)),f(c))


  IMPORTING unif_cont_fun   %% to maintain upward compatibility

END continuous_functions_more

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.