%------------------------------------------------------------------------------ % 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
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
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.
