%------------------------------------------------------------------------------
% Connected Spaces Definition
%
%     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/11/06  Initial Version
%------------------------------------------------------------------------------

connected_def[T:TYPE]: THEORY

BEGIN

  IMPORTING topology_prelim[T],
            topology_prelim[bool],
            topology,
            continuity_def,
            continuity

  U: VAR topology[T]
  f: VAR (surjective?[T,bool])

  connected_def:  LEMMA connected?(U) IFF
                  FORALL (A,B:(U)): nonempty?(A) AND nonempty?(B) =>
                                 NOT (disjoint?(A,B) AND Union(U) = union(A,B))

  connected_def2: LEMMA connected?(U) IFF
              FORALL f: NOT continuous?[T,(U),bool,discrete_topology[bool]](f)

END connected_def