Quelle  subspace.pvs

%------------------------------------------------------------------------------
% Topological subspaces
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            1/11/06  Initial Version
%     Version 1.1            8/6/06   Changed Interface, added type judgement
%------------------------------------------------------------------------------

subspace[T1:TYPE, (IMPORTING topology_def[T1]) S:topology,
         T2:TYPE FROM T1]: THEORY

BEGIN

  IMPORTING topology_def[T2]

  induced_topology: setofsets[T2] = image(restrict[T1,T2,bool],S)

  induced_subspace_topology: LEMMA topology?[T2](induced_topology)

  subspace_is_topology: JUDGEMENT induced_topology HAS_TYPE topology[T2]

END subspace