|
% sets ordered by "subset?" form a complete lattice
%
% Author: Alfons Geser, National Institute of Aerospace
% Date: Jan 2005
sets_complete_lattices[T: TYPE]: THEORY
BEGIN
IMPORTING booleans_are_finite, pointwise_orders[T, bool]
subset_equals_pointwise_implies: LEMMA
subset?[T] = pointwise(IMPLIES)
subset_is_a_complete_lattice: JUDGEMENT
subset?[T] HAS_TYPE (complete_lattice?[set[T]])
IMPORTING complete_lattices[set[T], subset?[T]]
END sets_complete_lattices
¤ Dauer der Verarbeitung: 0.16 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.
|
