%-------------------------------------------------------------------------
%
% The converse of Zorn's lemma: if every chain has a lower bound, then
% the set has a minimal element.
%
% For PVS version 3.2. January 17, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[T], relations[T], sets[T]
% orders: bounded_orders[T], chain[T,<=], converse_zorn[T,<=],
% minmax_orders[T], relations_extra[T]
%
%-------------------------------------------------------------------------
converse_zorn[T: TYPE, <=: (partial_order?[T])]: THEORY
EXPORTING ALL WITH orders[T], relations[T], sets[T], bounded_orders[T],
chain[T, <=], minmax_orders[T], relations_extra[T]
BEGIN
IMPORTING minmax_orders[T], chain[T, <=]
IMPORTING relation_converse_props[T], zorn[T, converse(<=)] % Proof only
converse_zorn: THEOREM
(FORALL (ch: chain[T, <=]): bounded_below?[T](ch, <=)) =>
(EXISTS (t: T): minimal?[T](t, fullset[T], <=))
END converse_zorn
¤ Dauer der Verarbeitung: 0.0 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.
|
