%------------------------------------------------------------------------------
% Lindelof's Covering Theorem
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            2/09/07  Initial Version
%------------------------------------------------------------------------------

lindelof[T:TYPE,(IMPORTING topology_def[T]) S:second_countable]: THEORY

BEGIN

  IMPORTING topology[T,S],
            sets_aux@countable_image % proof only

  U,V: VAR setofsets[T]

  lindelof: THEOREM open_cover?(U,fullset[T],S) =>
                    EXISTS V: is_countable(V) AND subcover?(V,U,fullset[T])

END lindelof