%------------------------------------------------------------------------------ % 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
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.11 Sekunden
(vorverarbeitet)
¤
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
