Quelle  topology_def.pvs

%------------------------------------------------------------------------------
% Topology definition file
%
%     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
%     Version 1.1            1/12/06  Basis material moved to basis.pvs (DRL)
%------------------------------------------------------------------------------

topology_def[T:TYPE]: THEORY

BEGIN

  S,B: VAR setofsets[T]

  IMPORTING topology_prelim[T],
            basis[T],
            sets_aux@countability

  has_countable_basis?(S):bool
    = EXISTS B: is_countable(B) AND synthetic_base?(B) AND
                synthetic_generated_topology_set(B) = S

  second_countable?(S):bool = topology?(S) AND has_countable_basis?(S)

  second_countable: TYPE = (second_countable?)

  second_countable_is_topology: JUDGEMENT second_countable SUBTYPE_OF topology

END topology_def