top: THEORY
%----------------------------------------------------------------------------
%
% Additional Set Theory (sets_aux)
% --------------------------------
%
% Version 1.0 Powersets merged with finite_sets_aux 2/10/04
% Version 2.0 Jerry James libraries added 5/5/04
% Version 2.1 Updates for PVS 3.2; removed theories 11/3/04
% now in the prelude or finite_sets
% Version 3.0 Merged in Alfons Geser's order theories 2/10/05
% Version 3.1 Added some theories from David Lester 4/12/05
% Version 3.2 Added cardinal and sets_lemmas_extra 5/11/05
% Version 3.3 Updated countable sets theories 9/15/09
%
% Authors:
% Bruno Dutertre <[email protected]> SRI International
% Jerry James <[email protected]> University of Kansas
% David Lester <[email protected]> Manchester University
%----------------------------------------------------------------------------
BEGIN
%---- Bruno Dutertre theories on powersets
IMPORTING
fun_below_props, % bijections with Cartesian products
power_sets, % cardinality and finiteness
set_of_functions % functions from finite set A to B
%---- Jerry James theories on infinite cardinalities
IMPORTING
bits, % sets of bit numbers (used to show countability)
card_comp, % compare the cardinality of any two types
card_comp_props, % properties of the card_comp predicates
card_comp_set, % compare the cardinality of any two sets
card_comp_set_props, % properties of the card_comp_set predicates
card_comp_set_transitive, % transitivity of the card_comp_set predicates
card_comp_transitive, % transitivity of the card_comp predicates
card_finite, % card_comp vs. card(S) from finite_sets
card_power, % card[T] < card[set[T]]
card_power_set, % card(S) < card(powerset(S))
card_sets_lemmas, % relationships of set operations to cardinality
card_single, % single type properties of card_comp_set preds
card_function, % surjection/injection image properties
cardinal, % cardinality(S) for any set S
countability, % definition of (un)countable sets
countable_image, % countable image
countable_props, % properties of (un)countable sets
countable_set, % some countable sets of numbers (e.g., integers)
countable_setofsets, % operations on countable families of sets
countable_types, % countability of some prelude types
infinite_card, % card_comp implications for finiteness
infinite_image, % infinite images of a set under some function
infinite_sets, % cardinality of infinite set add and remove
sets_lemmas_extra % disjoint? is commutative
%--- David Lester theories on infinite/countable sets
IMPORTING
countable_image, % image of a countable set is countable
card_function, % finite/infinite properties of functions
infinite_nat_def, % infinite IFF injective map from the naturals
indexed_sets_aux, % Additional prelude indexed set lemmas
countable_indexed_sets,% countable setsofsets vs indexed sets
nat_indexed_sets, % increasing/decresing indexed sets
inverse_image_Union, % inverse_image(f,Union(X))
countability_aux, %% RWB
cantor_bernstein_schroeder %% Proved by Anthony Narkawicz
IMPORTING
% Dragan Stosic's relational and functional choice facts based on Axiom of Choice
top_choice_facts,
% Dragan Stosic's refinement relations
top_refinement_relations
END top
¤ Dauer der Verarbeitung: 0.1 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.
|
