%-------------------------------------------------------------------------
%
% The cardinality of a set is always less than the cardinality of its
% power set.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% sets_aux: card_comp_set[set[T],T], card_comp_set[T,set[T]],
% card_comp_set_props[T,set[T]], card_power_set[T]
%
%-------------------------------------------------------------------------
card_power_set[T: TYPE]: THEORY
BEGIN
IMPORTING card_comp_set_props[T, set[T]]
card_power: THEOREM FORALL (S: set[T]): card_lt(S, powerset(S))
END card_power_set
¤ Dauer der Verarbeitung: 0.14 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.
|
