|
power_sets [T: TYPE ]: THEORY
%------------------------------------------------------------------------
% Power sets, finiteness and cardinality (Version 1.0) 6/28/96
%
% by Bruno Dutertre Royal Holloway & Bedford New College
%
% Establishes fundamental properties. The definition and finiteness
% proof have moved to the prelude.
%
%------------------------------------------------------------------------
EXPORTING ALL WITH finite_sets[nat], finite_sets[T], sets[T],
finite_sets_of_sets[T], set_of_functions[T, nat]
BEGIN
IMPORTING finite_sets@finite_sets_card_eq, finite_sets_of_sets[T], sets[T]
S, U: VAR set[T]
A: VAR finite_set[T]
n: VAR nat
B: finite_set[nat] = { n | n <= 1}
card_B: LEMMA card(B) = 2
IMPORTING set_of_functions[T, nat], finite_sets@finite_sets_eq
powerset_bijection : LEMMA (EXISTS (f: [(powerset(S)) -> [(S)->(B)]]):
bijective?(f))
finite_powerset_bijection: LEMMA (EXISTS (f: [(powerset(A))->(funset(A,B))]):
bijective?(f))
card_powerset : THEOREM card(powerset(A)) = 2 ^ card(A)
elem_finite_powerset : THEOREM (FORALL (X: (powerset(A))): is_finite(X))
SS: VAR set[set[T]]
finite_subset_of_powerset: THEOREM subset?(SS,powerset(A))
IMPLIES is_finite(SS)
END power_sets
¤ Dauer der Verarbeitung: 0.18 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.
|
