% every nonempty set of nats has a least element.
% This also holds for any subtype T of the integers.
%
% Author: Jerry James ([email protected]), University of Kansas
% Date: 13 Jan 2005
bounded_nats[T: TYPE FROM nat]: THEORY
BEGIN
IMPORTING bounded_integers[T]
every_nonempty_set_has_least: JUDGEMENT
(nonempty?[T]) SUBTYPE_OF (has_least?(<=))
END bounded_nats
¤ Dauer der Verarbeitung: 0.12 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.
|
