| Quellcodebibliothek Statistik Leitseite (Beweissystem der NASA Version 6.0.9©) |
Impressum 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 ¤ 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.0.13Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
