| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 904 B |
|
Quelle real_intervals.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28