Quellverzeichnis  compact_spaces.pvs

%------------------------------------------------------------------------------
% Compact Spaces
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Version 1.0            8/7/04   Initial Version
%------------------------------------------------------------------------------

compact_spaces[T:TYPE,(IMPORTING topology_prelim[T]) S:compact_space]: THEORY

BEGIN

  IMPORTING topology[T,S]

  U,V: VAR setofsets[T]

  compact_closed_def: LEMMA every(closed?,U)    AND                 % SKB 6.1.5
                            (FORALL V: subset?(V,U) AND is_finite(V) =>
                                              nonempty?(Intersection(V))) =>
                            nonempty?(Intersection(U))

END compact_spaces