%-------------------------------------------------------------------------
% Complete Measure Theory
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           04/05/09    Initial (DRL)
%-------------------------------------------------------------------------

complete_measure_theory[T:TYPE,          (IMPORTING subset_algebra_def[T])
                        S:sigma_algebra, (IMPORTING measure_def[T,S])
                        mu:complete_measure]: THEORY

BEGIN

  IMPORTING measure_space_def[T,S],
            sigma_algebra[T,S],
            measure_theory[T,S,mu],
            measure_props[T,S,mu]

  N: VAR null_set
  X: VAR set[T]
  E: VAR negligible
  f: VAR [T->real]
  g: VAR measurable_function

  null_subset:        LEMMA subset?(X,N)  => null_set?(X)
  null_is_negligible: LEMMA null_set?(X) <=> negligible_set?(X)
  ae_eq_measurable:   LEMMA ae_eq?(f,g)   => measurable_function?(f)

END complete_measure_theory