|
%------------------------------------------------------------------------------
% Extras for countability. Somewhere in sets_aux.
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
countability_aux[T:TYPE]: THEORY
BEGIN
IMPORTING countability[T],
countable_props[T]
t: VAR T
S: VAR set[T]
A,X,Y: VAR (is_countable)
countably_infinite_is_nonempty: JUDGEMENT
countably_infinite_set SUBTYPE_OF (nonempty?[T])
countably_infinite_is_infinite: JUDGEMENT
countably_infinite_set SUBTYPE_OF (is_infinite[T])
countable_emptyset: LEMMA is_countable(emptyset[T])
countable_singleton: LEMMA is_countable(singleton(t))
countable_add: LEMMA is_countable(add(t,X))
countable_remove: LEMMA is_countable(remove(t,X))
countable_intersection1: LEMMA is_countable(intersection(X,S))
countable_intersection2: LEMMA is_countable(intersection(S,X))
countable_difference: LEMMA is_countable(difference(X,S))
END countability_aux
¤ Dauer der Verarbeitung: 0.15 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.
|
