Quelle  real_intervals.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