SSL hausdorff_convergence.pvs

%------------------------------------------------------------------------------
% Hausdorff convergence
%
%     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            06/09/06  Initial Version
%------------------------------------------------------------------------------

hausdorff_convergence[T:TYPE,(IMPORTING topology_def[T]) S:hausdorff]: THEORY

BEGIN

  IMPORTING topological_convergence[T,S]

  u:         VAR sequence[T]
  v:         VAR convergent
  x,l,l1,l2: VAR T

  unique_limit: LEMMA convergence?(u,l1) AND convergence?(u,l2) => l1 = l2

  limit_def:    LEMMA limit(v) = l IFF convergence?(v, l)

  singleton_is_closed: JUDGEMENT singleton(x) HAS_TYPE closed

  compact_is_closed:   JUDGEMENT compact SUBTYPE_OF closed              % 5.4.2

END hausdorff_convergence