|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
