|
% 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.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
