Quelle  connected_set.pvs

%------------------------------------------------------------------------------
% connected_set
% All type of intervals are connected sets
%------------------------------------------------------------------------------

connected_set : THEORY
BEGIN

   x,y : VAR real
                  
   Connected : TYPE = 
     {s:set[real] | FORALL (a,b:(s)),(c:real): a <= c AND c <= b IMPLIES s(c)}

   ConnectedGt(x)     : TYPE = {s:Connected | FORALL (z:(s)): z > x}

   ConnectedGe(x)     : TYPE = {s:Connected | FORALL (z:(s)): z >= x}

   ConnectedLt(x)     : TYPE = {s:Connected | FORALL (z:(s)): z < x}

   ConnectedLe(x)     : TYPE = {s:Connected | FORALL (z:(s)): z <= x}

   ConnectedGtLt(x,y) : TYPE = {s:Connected | FORALL (z:(s)): x < z AND z < y}

   ConnectedGtLe(x,y) : TYPE = {s:Connected | FORALL (z:(s)): x < z AND z <= y}

   ConnectedGeLt(x,y) : TYPE = {s:Connected | FORALL (z:(s)): x <= z AND z < y}

   ConnectedGeLe(x,y): TYPE = {s:Connected | FORALL (z:(s)): x <= z AND z <= y}

   % (x,...)
   OpenInf(x) : ConnectedGt(x) = {z:real | z > x}

   % [x,...)
   CloseInf(x) : ConnectedGe(x) = {z:real | z >= x}

   % (...,x)
   InfOpen(x) : ConnectedLt(x) = {z:real | z < x}

   % (...,x]
   InfClose(x) : ConnectedLe(x) = {z:real | z <= x}

   % (x,y)
   OpenOpen(x,y) : ConnectedGtLt(x,y) = {z:real | x < z AND z < y}

   % (x,y]
   OpenClose(x,y) : ConnectedGtLe(x,y) = {z:real | x < z AND z <= y}

   % [x,y)
   CloseOpen(x,y) : ConnectedGeLt(x,y) = {z:real | x <= z AND z < y}

   % [x,y]
   CloseClose(x,y) : ConnectedGeLe(x,y) = {z:real | x <= z AND z <= y}

END connected_set