|
%------------------------------------------------------------------------------
% 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.14 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
