Quelle  top_basic.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Basic Topological Properties
%
%     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            1/12/06  Initial Version
%------------------------------------------------------------------------------

top_basic: THEORY

BEGIN

  IMPORTING topology_prelim,    % Preliminary Definitions for topology
            basis,              % Defining the basis of a topology
            topology_def,       % Basic Definitions for topology
            topology,           % Further properties of topologies
            subspace,           % subspace properties
            lindelof,           % Lindelof covering theorem

            cross_product        %% RWB


END top_basic