products/Sources/formale Sprachen/JAVA/openjdk-20-36_src/src/hotspot/share/adlc/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: PVS

Original von: PVS©
%------------------------------------------------------------------------------
% Completeness of Essential Bounds
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            19/3/11   Initial Version
%------------------------------------------------------------------------------

essential_bound_complete_scaf[
                    (IMPORTING measure_integration@subset_algebra_def,
                               measure_integration@measure_def)
                    T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S]]: THEORY

BEGIN

  IMPORTING essentially_bounded[T,S,mu],
            topology@subseq[essentially_bounded], % Proof only
            complex_topology                      % Proof only

  F: VAR sequence[essentially_bounded]
  f: VAR essentially_bounded
  r: VAR posreal
  i,j,n: VAR nat

  essential_bound_complete_scaf: LEMMA
      (FORALL r: EXISTS n: FORALL i,j: i >= n AND j >= n =>
           essential_bound(F(j)-F(i)) < r)
    IMPLIES
      (EXISTS f: FORALL r: EXISTS n: FORALL i: i >= n =>
           essential_bound(f-F(i)) < r)

END essential_bound_complete_scaf

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff