|
%------------------------------------------------------------------------------
% Heine-Borel for the real topology
%
% Author: David Lester, Manchester University
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Version 1.0 17/08/07 Initial Version
%
% Notes: The statement of the theorem is capable of considerable
% generalization. I just need a result for the reals now.
% I suspect that the generalized proof is probably easier too.
%
% It isn't (easier)! The result is in metric_space, lemma
%
% compact_is_complete_totally_bounded
%------------------------------------------------------------------------------
heine_borel_scaf: THEORY
BEGIN
IMPORTING real_topology,
reals@bounded_reals[real]
a,b,x: VAR real
U,C: VAR setofsets[real]
heine_borel_aux: THEOREM
a <= b AND every(open?,C) AND
open_cover?(C,{x| a <= x AND x <= b},metric_induced_topology) =>
EXISTS U: subset?(U,C) AND is_finite(U) AND
subset?({x| a <= x AND x <= b},Union(U))
END heine_borel_scaf
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
