Quelle  product_sigma_def.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Product sigma algebras
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian, "Fundamentals of Real Analysis"
% Springer, 1999
%
%     Version 1.0            11/09/08  Initial Version
%------------------------------------------------------------------------------

product_sigma_def[T1,T2:TYPE]: THEORY

BEGIN

  IMPORTING subset_algebra_def,
            sigma_algebra,
            topology@cross_product[T1,T2],
            product_sections[T1,T2],
            sets_aux@countable_image % Proof Only

  i,n: VAR nat
  x:  VAR T1
  y:  VAR T2
  X:  VAR set[T1]
  Y:  VAR set[T2]
  NX: VAR (nonempty?[T1])
  NY: VAR (nonempty?[T2])
  Z:  VAR set[[T1,T2]]
  S1: VAR sigma_algebra[T1]
  S2: VAR sigma_algebra[T2]

  measurable_rectangle?(S1,S2)(Z):bool
    = EXISTS X,Y: Z = cross_product(X,Y) AND S1(X) AND S2(Y)

  measurable_rectangle(S1,S2): TYPE+ = (measurable_rectangle?(S1,S2))
                                                           CONTAINING emptyset


  sigma_times(S1,S2):sigma_algebra[[T1,T2]]
    = generated_sigma_algebra(fullset[measurable_rectangle(S1,S2)])

  x_section_measurable:   LEMMA member(Z,sigma_times(S1,S2)) =>
                                member(x_section(Z,x),S2)
  y_section_measurable:   LEMMA member(Z,sigma_times(S1,S2)) =>
                                member(y_section(Z,y),S1)

  sigma_cross_projection: LEMMA                                         % 7.2.7
     member(cross_product(NX,NY),sigma_times(S1,S2)) =>
     (member(NX,S1) AND member(NY,S2))

END product_sigma_def