Top File of PVS lebesgue Library

 
%------------------------------------------------------------------------------
% Top file for Lebesgue Integration
%
%     Author: David Lester, Manchester University
%
% References: AJ Weir, "Lebesgue Integration and Measure" CUP, 1973.
%
%     Version 1.0            26/2/10   Initial Version
%
% In order for this theory to typecheck, you must first kill bins (i.e. rm pvsbin/*.bin) in
%
%     measure_integration
%     metric_space
%
%------------------------------------------------------------------------------

top: THEORY

BEGIN

  IMPORTING

% Extras for Metric Space
    bounded_interval_props,
    continuous_on,      % continuity on subsets
    real_intervals_aux, % Bounded Intervals
    real_intervals,     % Often-used intervals
    tends,

% Extras for analysis
    restriction_integral,  % restrict/extend for analysis Integrals

% Lebesgue definition
    real_lebesgue_scaf ,   % Old version of lebesgue definition
    lebesgue_def,          % Definition of lebesgue measure (lambda_),
                           %   and measurable sets (cal_M)

% Riemann-Lebesgue link
    ae_continuous_def,     % definitions of ae continuity
    riemann_scaf,          % link scaffolding
    riemann_link,          % link
    lebesgue_fundamental   % Fundamental Theorem of Calculus for Lebesgue
                           %     (includes integration by parts)

END top

The tag identifies links that are outside the NASA domain