Details About PVS Complex Library

This library contains various theories related to sets. It contains Bruno Dutertre's theories on powersets:

  fun_below_props,          % bijections with Cartesian products
  power_sets,               % cardinality and finiteness
  set_of_functions          % functions from finite set A to B

It also contains Jerry James's theories on set cardinality for both finite and infinite sets:

  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
  countability,             % definition of (un)countable sets
  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

The library also contains David Lester's additions to the infinite cardinality theories:

  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

Finally, the library also contains Alfons Geser's proof that the image of an arbitrary function on a finite set is also a finite set:

  finite_function_image     % the function image of a finite set is finite