% every above (below) bounded, non-empty set of integers has a greatest
% (least) element. This also holds for any subtype T of the integers.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: 2003/04
%
% remove_greatest, remove_greatest_monotone, intersection_greatest, and
% intersection_least added 13 Jan 2005 by Jerry James ([email protected]),
% University of Kansas
bounded_integers[T: TYPE FROM int]: THEORY
BEGIN
IMPORTING
non_empty_bounded_sets[T]
Su, Su1, Su2: VAR (non_empty_bounded_above?)
Sl, Sl1, Sl2: VAR (non_empty_bounded_below?)
i, j: VAR T
S: VAR set[T]
c: VAR nat
non_empty_bounded_above_has_greatest_lem: LEMMA
S(i) & upper_bound?[T](j, S, <=) & c = j - i => has_greatest?(S, <=)
non_empty_bounded_above_has_greatest: JUDGEMENT
(non_empty_bounded_above?) SUBTYPE_OF (has_greatest?(<=))
non_empty_bounded_below_has_least_lem: LEMMA
S(i) & lower_bound?[T](j, S, <=) & c = i - j => has_least?(S, <=)
non_empty_bounded_below_has_least: JUDGEMENT
(non_empty_bounded_below?) SUBTYPE_OF (has_least?(<=))
remove_least: LEMMA
nonempty?(remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl),
Sl)) =>
least[T](restrict[[real, real], [T, T], bool](<=))(Sl) <
least[T](restrict[[real, real], [T, T], bool](<=))(
remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl), Sl))
remove_least_monotone: LEMMA
subset?(Sl1, Sl2) =>
subset?(
remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1), Sl1),
remove(least[T](restrict[[real, real], [T, T], bool](<=))(Sl2), Sl2))
remove_greatest: LEMMA
nonempty?(remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su),
Su)) =>
greatest[T](restrict[[real, real], [T, T], bool](<=))(
remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su), Su))
< greatest[T](restrict[[real, real], [T, T], bool](<=))(Su)
remove_greatest_monotone: LEMMA
subset?(Su1, Su2) =>
subset?(
remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1), Su1),
remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2), Su2))
intersection_greatest: LEMMA
disjoint?(Su1, Su2) OR has_greatest?(intersection(Su1, Su2), <=)
intersection_least: LEMMA
disjoint?(Sl1, Sl2) OR has_least?(intersection(Sl1, Sl2), <=)
END bounded_integers
¤ Dauer der Verarbeitung: 0.0 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.
|
