|
%------------------------------------------------------------------------------
% Sigma Algebra
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
sigma_algebra[T:TYPE,(IMPORTING subset_algebra_def[T])
S:sigma_algebra]: THEORY
BEGIN
IMPORTING subset_algebra[T,S],
sets_aux@countable_image % Proof only
x,y: VAR (S)
SS: VAR sequence[(S)]
sigma_algebra_emptyset: LEMMA member(emptyset[T],S)
sigma_algebra_fullset: LEMMA member(fullset[T],S)
sigma_algebra_complement: LEMMA member(complement(x),S)
sigma_algebra_union: LEMMA member(union(x,y),S)
sigma_algebra_intersection: LEMMA member(intersection(x,y),S)
sigma_algebra_difference: LEMMA member(difference(x,y),S)
sigma_algebra_IUnion: LEMMA member(IUnion(SS),S)
sigma_algebra_IIntersection: LEMMA member(IIntersection(SS),S)
sigma_algebra_emptyset_rew: JUDGEMENT emptyset[T] HAS_TYPE (S)
sigma_algebra_fullset_rew: JUDGEMENT fullset[T] HAS_TYPE (S)
sigma_algebra_complement_rew: JUDGEMENT complement(x) HAS_TYPE (S)
sigma_algebra_union_rew: JUDGEMENT union(x,y) HAS_TYPE (S)
sigma_algebra_intersection_rew: JUDGEMENT intersection(x,y) HAS_TYPE (S)
sigma_algebra_difference_rew: JUDGEMENT difference(x,y) HAS_TYPE (S)
sigma_algebra_IUnion_rew: JUDGEMENT IUnion(SS) HAS_TYPE (S)
sigma_algebra_IIntersection_rew: JUDGEMENT IIntersection(SS) HAS_TYPE (S)
END sigma_algebra
¤ Dauer der Verarbeitung: 0.0 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.
|
