|
%------------------------------------------------------------------------------
% 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
[ zur Elbe Produktseite wechseln0.3Quellennavigators
Analyse erneut starten
]
|
