| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/complex_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle essential_bound_complete_scaf.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Completeness of Essential Bounds % % Author: David Lester, Manchester University % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 19/3/11 Initial Version %------------------------------------------------------------------------------ essential_bound_complete_scaf[ (IMPORTING measure_integration@subset_algebra_def, measure_integration@measure_def) T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S]]: THEORY BEGIN IMPORTING essentially_bounded[T,S,mu], topology@subseq[essentially_bounded], % Proof only complex_topology % Proof only F: VAR sequence[essentially_bounded] f: VAR essentially_bounded r: VAR posreal i,j,n: VAR nat essential_bound_complete_scaf: LEMMA (FORALL r: EXISTS n: FORALL i,j: i >= n AND j >= n => essential_bound(F(j)-F(i)) < r) IMPLIES (EXISTS f: FORALL r: EXISTS n: FORALL i: i >= n => essential_bound(f-F(i)) < r) END essential_bound_complete_scaf ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28