Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: fundamental_algebra.prf Sprache: PVS

Original von: PVS^©

integral_diff_doms[T: TYPE+ FROM real, U: TYPE+ FROM real]: THEORY
%----------------------------------------------------------------------------
%
%  Integral of two functions that are identical over the integration
%  range and have different domains are shown to be equal.
%
%  Author:  Rick Butler     NASA Langley Research Center
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING
      IMPORTING deriv_domain_def

      connected_domain : ASSUMPTION connected?[T]

      not_one_element  : ASSUMPTION not_one_element?[T]

      con_dom_U        : ASSUMPTION  connected?[U]

      not_one_U        : ASSUMPTION not_one_element?[U]

   ENDASSUMING

   IMPORTING integral

   f: VAR [T -> real]
   g: VAR [U -> real]

   a,b: VAR real

   int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND
                       U_pred(a) AND U_pred(b) AND a < b AND
                       integrable?[T](a,b,f) AND integrable?[U](a, b, g) AND
                   (FORALL (x: real): x >= a AND x <= b IMPLIES f(x) = g(x))
               IMPLIES
                    integral(a,b,f) = integral(a,b,g)

   Int_diff_dom: LEMMA T_pred(a) AND T_pred(b) AND
                       U_pred(a) AND U_pred(b) AND
                       Integrable?[T](a,b,f) AND Integrable?[U](a, b, g) AND
                   (FORALL (x: Closed_interval[real](a,b)): f(x) = g(x))
               IMPLIES
                    Integral(a,b,f) = Integral(a,b,g)


END integral_diff_doms

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.