| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 489 B |
|
Quelle sets_complete_lattices.pvs Sprache: PVS |
|||||||||
|
% 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.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28