Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 13 kB image not shown  

SSL lim_of_composition.pvs   Interaktion und
PortierbarkeitPVS

 
lim_of_composition [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%  Author:  Bruno Dutertre    Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN

  IMPORTING lim_of_functions, continuous_functions[T2]

  f : VAR [T1 -> T2]
  g : VAR [T2 -> real]

  x, y : VAR real
  z : VAR T2

  l : VAR real


  adherence_lemma  : LEMMA convergence(f, x, y) 
                             IMPLIES adh[T2](fullset[real])(y)
        
  adherence_lemma2 : LEMMA convergent?(f, x) 
                             IMPLIES adh[T2](fullset[real])(lim(f, x))


  convergence_composition : LEMMA convergence(f, x, y) AND convergence(g, y, l)
                             IMPLIES convergence(g o f, x, l)

  convergent_composition  : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
                             IMPLIES convergent?(g o f, x)

  lim_composition         : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
                             IMPLIES lim(g o f, x) = lim(g, lim(f, x))


  convergence_comp_continuous: LEMMA convergence(f, x, z) AND continuous?(g, z) 
                                 IMPLIES convergence(g o f, x, g(z))

  convergent_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
                              AND continuous?(g, lim(f, x))
                                 IMPLIES convergent?(g o f, x)

  lim_comp_continuous        : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
                              AND continuous?(g, lim(f, x))
                              IMPLIES
                                   lim(g o f, x) = g(lim(f, x))

END lim_of_composition

93%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.11Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




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.