Quellcode-Bibliothek continuous_functions_more.pvs Sprache: 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

quality93%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.