| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 904 B |
|
Quellcode-Bibliothek kuratowski.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Kuratowski's lemma: there exists a maximal chain. This is equivalent % to Zorn's lemma and the Axiom of Choice. % % For PVS version 3.2. January 17, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: orders[chain[T,<=]], orders[T], sets[T] % orders: chain[T,<=], kuratowski[T,<=] % %------------------------------------------------------------------------- kuratowski[T: TYPE, <=: (partial_order?[T])]: THEORY % Hide the imports used only in the proof EXPORTING ALL WITH orders[T], sets[T], orders[chain[T, <=]], chain[T, <=] BEGIN IMPORTING chain_chain[T, <=], zorn[subchain, chain_incl] kuratowski: THEOREM EXISTS (ch: chain[T, <=]): maximal_chain?[T, <=](ch) END kuratowski ¤ 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.0.12Bemerkung: (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
