%-------------------------------------------------------------------------
%
% 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 ([email protected]), 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
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
