%------------------------------------------------------------------------------ % 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
¤ Dauer der Verarbeitung: 0.10 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.
