% non-empty sets of reals that are bounded from above or below.
% These are exactly the sets that have least upper (greatest lower) bounds.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004
%
% non_empty_finite_bounded_above and non_empty_finite_bounded_below added
% 13 Jan 2005 by Jerry James ([email protected]), University of Kansas
non_empty_bounded_sets[T: TYPE FROM real]: THEORY
BEGIN
IMPORTING total_lattices[T, <=]
non_empty_bounded_above?(S: set[T]): bool =
nonempty?[T](S) & bounded_above?[T](<=)(S)
non_empty_bounded_below?(S: set[T]): bool =
nonempty?[T](S) & bounded_below?[T](<=)(S)
non_empty_bounded_above_is_nonempty: JUDGEMENT
(non_empty_bounded_above?) SUBTYPE_OF (nonempty?[T])
non_empty_bounded_above_is_bounded_above: JUDGEMENT
(non_empty_bounded_above?) SUBTYPE_OF (bounded_above?[T](<=))
non_empty_bounded_below_is_nonempty: JUDGEMENT
(non_empty_bounded_below?) SUBTYPE_OF (nonempty?[T])
non_empty_bounded_below_is_bounded_below: JUDGEMENT
(non_empty_bounded_below?) SUBTYPE_OF (bounded_below?[T](<=))
non_empty_finite_bounded_above: JUDGEMENT
non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_above?)
non_empty_finite_bounded_below: JUDGEMENT
non_empty_finite_set[T] SUBTYPE_OF (non_empty_bounded_below?)
END non_empty_bounded_sets
¤ Dauer der Verarbeitung: 0.65 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.
|
