| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/metric_space/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle heine_borel_scaf.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% 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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28