Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Emacs_Insert_File.bsh
Sprache: Unknown
%-------------------------------------------------------------------------
%
% Operations on countable families of sets.
%
% For PVS version 3.2. February 10, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[finite_set[T]], finite_sets[set[T]], finite_sets[T],
% infinite_sets_def[finite_set[T]], infinite_sets_def[set[T]],
% infinite_sets_def[T]
% sets_aux: card_comp_set[finite_set[T],finite_set[T]],
% card_comp_set[finite_set[T],nat], card_comp_set[nat,finite_set[T]],
% card_comp_set[nat,set[T]], card_comp_set[nat,T],
% card_comp_set[set[T],nat], card_comp_set[set[T],set[T]],
% card_comp_set[set[T],T], card_comp_set[T,nat], card_comp_set[T,set[T]],
% card_comp_set[T,T], card_comp_set_props[finite_set[T],finite_set[T]],
% card_comp_set_props[finite_set[T],nat], card_comp_set_props[set[T],nat],
% card_comp_set_props[set[T],set[T]], card_comp_set_props[T,nat],
% card_comp_set_props[T,set[T]], card_comp_set_props[T,T],
% card_comp_set_transitive[nat,T,set[T]], card_comp_set_transitive[nat,T,T],
% card_power_set[T], card_sets_lemmas[T], card_single[finite_set[T]],
% card_single[set[T]], card_single[T], countability[finite_set[T]],
% countability[set[T]], countability[T], countable_props[finite_set[T]],
% countable_props[set[T]], countable_props[T], countable_set,
% countable_setofsets[T]
%
%-------------------------------------------------------------------------
countable_setofsets[T: TYPE]: THEORY
BEGIN
IMPORTING countable_set,
countable_props[T],
countable_props[set[T]],
countable_props[finite_set[T]]
S: VAR setofsets[T]
countable_union1: THEOREM
FORALL S:
is_countable[set[T]](S) AND every(is_countable)(S) =>
is_countable[T](Union(S))
%% Note that the converse of conutable_union1 is not quite true; it is
%% possible to have an uncountable set whose union is countable. For
%% example, consider the set of natural numbers. Its power set is
%% uncountable, and the union of the power set is the (countable) set of
%% natural numbers.
countable_union2: THEOREM
FORALL S: is_countable[T](Union(S)) => every(is_countable)(S)
countable_intersection: THEOREM
FORALL S:
nonempty?(S) AND every(is_countable)(S) =>
is_countable(Intersection(S))
%% The finite subsets of a given set. For a finite set, this is the
%% powerset. Otherwise, it is the finite elements of the powerset.
finite_subsets(S: set[T]): set[finite_set[T]] =
{F: finite_set[T] | subset?(F, S)}
countable_finite_subsets: JUDGEMENT
finite_subsets(S: countable_set[T]) HAS_TYPE countable_set[finite_set[T]]
countably_infinite_finite_subsets: JUDGEMENT
finite_subsets(S: countably_infinite_set[T])
HAS_TYPE countably_infinite_set[finite_set[T]]
END countable_setofsets
[ zur Elbe Produktseite wechseln0.0Quellennavigators
Analyse erneut starten
]
|
|
