Quelle real_intervals.pvs Sprache: 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

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

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.