Quelle  sigma_algebra.pvs

%------------------------------------------------------------------------------
% 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