|
real_sets[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------
%
% Adapted by Rick Butler from theory that was
% developed by Bruno Dutertre
%
% Fundamental definitions are in bounded_reals.
%
%------------------------------------------------------------------------
BEGIN
IMPORTING bounded_reals[T]
S,S1,S2: VAR (nonempty?[T])
U,U1,U2: VAR sup_set % { S | (EXISTS a : upper_bound?(<=)(a, S))}
V,V1,V2: VAR inf_set % { S | (EXISTS a : lower_bound?(<=)(a, S))}
W,W1,W2: VAR max_set % { S | (EXISTS c : S(c) AND upper_bound?(<=)(c, S)}
X,X1,X2: VAR min_set % { S | (EXISTS c : S(c) AND lower_bound?(<=)(c, S)}
a, x: VAR real
c: VAR T
sup_lemma : LEMMA least_upper_bound(<=)(sup(U), U)
sup_is_bound : COROLLARY (FORALL (y: (U)) : y <= sup(U))
sup_is_bound2 : COROLLARY upper_bound(<=)(sup(U), U)
sup_is_sup : COROLLARY upper_bound(<=)(x, U) IFF sup(U) <= x
upper_bound_subset : LEMMA subset?(S1, S2) AND upper_bound(<=)(a, S2)
IMPLIES upper_bound(<=)(a, S1)
subset_above_bounded : COROLLARY subset?(S, U) IMPLIES above_bounded(S)
sup_of_subset : COROLLARY subset?(U1, U2) IMPLIES sup(U1) <= sup(U2)
adherence_sup : THEOREM (FORALL (epsilon: posreal):
(EXISTS (y: (U)) : sup(U) - epsilon < y))
inf_lemma : LEMMA greatest_lower_bound(<=)(inf(V), V)
inf_is_bound : COROLLARY (FORALL (y: (V)) : inf(V) <= y)
inf_is_bound2 : COROLLARY lower_bound(<=)(inf(V), V)
inf_is_inf : COROLLARY lower_bound(<=)(x, V) IFF x <= inf(V)
lower_bound_subset : LEMMA subset?(S1, S2) and lower_bound(<=)(a, S2)
IMPLIES lower_bound(<=)(a, S1)
subset_below_bounded : COROLLARY subset?(S, V) IMPLIES below_bounded(S)
inf_of_subset : COROLLARY subset?(V1, V2) IMPLIES inf(V2) <= inf(V1)
adherence_inf : THEOREM (FORALL (epsilon: posreal):
(EXISTS (y: (V)) : y < inf(V) + epsilon))
END real_sets
¤ Dauer der Verarbeitung: 0.15 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.
|
