%------------------------------------------------------------------------------ % 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
[ Verzeichnis aufwärts0.15unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
