Quelle countable_setofsets.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  Operations on countable families of sets.
%
%  For PVS version 3.2.  February 10, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), 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

quality95%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.