%------------------------------------------------------------------------------ % Properties of bounded intervals % % Author: David Lester, Manchester University % % Version 1.0 26/2/10 Initial Version %------------------------------------------------------------------------------
bounded_interval_props: THEORY
BEGIN
IMPORTING real_intervals_aux
A,B: VAR bounded_interval
a,b: VAR real
bounded_interval1: LEMMA A(a) => inf(A) <= a AND a <= sup(A)
bounded_interval2: LEMMAnonempty?[real](A) AND inf(A) < a AND a < sup(A)
=> A(a)
bounded_interval3: LEMMAnonempty?[real](A) => inf(A) <= sup(A)
bounded_interval4: LEMMA disjoint?[real](A,B) AND A(a) AND B(b) AND a <= b =>
sup(A) <= inf(B)
bounded_interval5: LEMMA disjoint?[real](A,B) AND A(a) AND B(b) AND a <= b => FORALL (x:(A),y:(B)): x < y
bounded_interval_disjoint_union1: LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
A(a) AND B(b) AND a <= b =>
sup(A) = inf(B)
bounded_interval_disjoint_union2: LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
A(a) AND B(b) AND a <= b =>
(A(sup(A)) OR B(inf(B)))
bounded_interval_disjoint_union3: LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
A(a) AND B(b) AND a <= b =>
inf(union[real](A,B)) = inf(A)
bounded_interval_disjoint_union4: LEMMA disjoint?[real](A,B) AND bounded_interval?(union[real](A,B)) AND
A(a) AND B(b) AND a <= b =>
sup(union[real](A,B)) = sup(B)
END bounded_interval_props
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
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.
