%------------------------------------------------------------------------------
% 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[T1,T2:TYPE, (IMPORTING subset_algebra_def)
              S1:sigma_algebra[T1],
              S2:sigma_algebra[T2]]: THEORY

BEGIN

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

  n,i: VAR nat
  X: VAR (S1)
  Y: VAR (S2)
  x: VAR T1
  y: VAR T2
  Z: VAR set[[T1,T2]]
  NX: VAR (nonempty?[T1])
  NY: VAR (nonempty?[T2])
  R,R1,R2: VAR set[(measurable_rectangle?(S1,S2))]
  r,r1,r2: VAR (measurable_rectangle?(S1,S2))

  cross_product_is_sigma_times: LEMMA sigma_times(S1,S2)(cross_product(X,Y))

  rectangle_algebra_aux: LEMMA
    generated_subset_algebra[[T1,T2]](measurable_rectangle?(S1,S2))
      = finite_disjoint_unions[[T1,T2]](measurable_rectangle?(S1,S2))

  rectangle_algebra:subset_algebra[[T1,T2]]                        % SKB 7.2.2
    = finite_disjoint_unions[[T1,T2]](measurable_rectangle?(S1,S2))

  rectangle_algebra_def: LEMMA
    rectangle_algebra
      = generated_subset_algebra[[T1,T2]](measurable_rectangle?(S1,S2))

  finite_disjoint_rectangles: LEMMA
    finite_disjoint_unions[[T1,T2]](measurable_rectangle?(S1,S2))(Z) <=>
    EXISTS R: Union(R) = Z  AND is_finite(R) AND
           FORALL (x,y:(R)): x = y OR disjoint?(x,y)

  intersection_rectangle: LEMMA
    finite_disjoint_union?(measurable_rectangle?(S1,S2))(intersection(r1,r2))

  complement_rectangle:   LEMMA
    finite_disjoint_union?(measurable_rectangle?(S1,S2))(complement(r))

END product_sigma