%------------------------------------------------------------------------------
% Monotone Class Lemma for finite measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

monotone_classes[T:TYPE,C:(nonempty?[set[T]])]: THEORY

BEGIN

  IMPORTING subset_algebra_def[T]

  a,b: VAR (C)
  x:   VAR (generated_sigma_algebra(C))

  IMPORTING measure_def[T,(generated_sigma_algebra(C))],
            sigma_algebra,                                % Proof Only
            measure_props                                 % Proof Only

  monotone_finite_measures: COROLLARY FORALL (nu,mu:finite_measure):    % 4.6.7
    (FORALL a,b: member(intersection(a,b),C))              AND
    (FORALL a:   finite_disjoint_union?(C)(complement(a))) AND
    (FORALL a:   mu(a) = nu(a))                            =>
    (FORALL x:   mu(x) = nu(x))

END monotone_classes