%-------------------------------------------------------------------------
%
% Cardinality properties of infinite sets.
%
% For PVS version 3.2. February 10, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[T], infinite_sets_def[T]
% sets_aux: card_comp_set[nat,T], card_comp_set[T,nat], card_comp_set[T,T],
% card_comp_set_props[T,nat], card_comp_set_props[T,T],
% card_sets_lemmas[T], card_single[T], countable_props[T],
% countability[T], infinite_sets[T]
%
%-------------------------------------------------------------------------
infinite_sets[T: TYPE]: THEORY
BEGIN
IMPORTING countable_props[T], card_sets_lemmas[T]
t: VAR T
S, R: VAR set[T]
Fin: VAR finite_set[T]
Inf: VAR infinite_set[T]
infinite_add_card: THEOREM FORALL Inf, t: card_eq(Inf, add(t, Inf))
infinite_remove_card: THEOREM FORALL Inf, t: card_eq(Inf, remove(t, Inf))
finite_infinite_lt: THEOREM
FORALL S: (FORALL Fin: card_lt(Fin, S)) IFF is_infinite(S)
END infinite_sets
¤ 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.
|
