Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: real_intervals.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Real Intervals
%
%     Author: David Lester, Manchester University
%
% A neater way to express the usual sets over which we integrate
%
% In particular, with proper definition of the display functions we
% get
%        integral(open_inf(a),f)
% as
%        $\int_{(a,\inf)} f$
%
% Also, the great counter-example integral(rationals,f)
% as     $\int_{\mathbb Q} f$
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

real_intervals: THEORY

BEGIN

  IMPORTING metric_space@real_topology

  x: VAR real

  IMPORTING
    measure_integration@hausdorff_borel[real,metric_induced_topology],
    sets_aux@countable_image, % Proof Only
    power@rational_props_aux  % Proof Only

  rationals:borel = {x | rational_pred(x)}

END real_intervals

¤ Dauer der Verarbeitung: 0.0 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.