The abstract of the Mizar article:

Completeness of the $\sigma$-Additive Measure. Measure Theory

by

Jozef Bialas

Received February 22, 1992

MML identifier: MEASURE3

[ Mizar article, MML identifier index ]

environ

 vocabulary SUPINF_1, FUNCT_1, SUPINF_2, ARYTM_3, ORDINAL2, RELAT_1, MEASURE1,
      MEASURE2, SETFAM_1, BOOLE, TARSKI, ARYTM_1, RLVECT_1, PROB_1, MEASURE3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1,
      FUNCT_1, FUNCT_2, REAL_1, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1,
      MEASURE2;
 constructors NAT_1, REAL_1, SUPINF_2, MEASURE2, PROB_2, MEMBERED, XBOOLE_0;
 clusters SUBSET_1, SUPINF_1, MEASURE1, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
      XBOOLE_0, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin
::
::             Some additional properties about R_eal numbers
::

 reserve X for set;

theorem :: MEASURE3:1
     for x being R_eal holds
   (-infty <'x & x <'+infty) implies x is Real;

theorem :: MEASURE3:2
   for x being R_eal holds
   ((not x = -infty) & (not x = +infty)) implies x is Real;

theorem :: MEASURE3:3
   for F1,F2 being Function of NAT,ExtREAL st
   (for n being Nat holds Ser(F1).n <=' Ser(F2).n) holds
   (SUM(F1) <=' SUM(F2));

theorem :: MEASURE3:4
     for F1,F2 being Function of NAT,ExtREAL holds
   ((for n being Nat holds Ser(F1).n = Ser(F2).n) implies
   (SUM(F1) = SUM(F2)));

::
::         Some additional theorems about measures and functions
::

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   redefine mode N_Measure_fam of S;
    synonym N_Sub_fam of S;
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let F be Function of NAT,S;
   redefine func rng F -> N_Measure_fam of S;
end;

theorem :: MEASURE3:5
     for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       F being Function of NAT,S,
       A being Element of S holds
   (meet rng F c= A & (for n being Element of NAT holds A c= F.n)) implies
   M.A = M.(meet rng F);

theorem :: MEASURE3:6
   for S being sigma_Field_Subset of X holds
   for G,F being Function of NAT,S holds
       (G.0 = {} & for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies
       union rng G = F.0 \ meet rng F;

theorem :: MEASURE3:7
   for S being sigma_Field_Subset of X holds
   for G,F being Function of NAT,S holds
       (G.0 = {} & for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n)) implies
       meet rng F = F.0 \ union rng G;

theorem :: MEASURE3:8
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       M.(meet rng F) = M.(F.0) - M.(union rng G);

theorem :: MEASURE3:9
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       M.(union rng G) = M.(F.0) - M.(meet rng F);

theorem :: MEASURE3:10
     for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} & for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       M.(meet rng F) = M.(F.0) - sup(rng (M*G));

theorem :: MEASURE3:11
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} &
        for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       sup(rng (M*G)) is Real & M.(F.0) is Real & inf(rng (M*F)) is Real;

theorem :: MEASURE3:12
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} &
        for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       sup(rng (M*G)) = M.(F.0) - inf(rng (M*F));

theorem :: MEASURE3:13
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for G,F being Function of NAT,S holds
       (M.(F.0) <'+infty & G.0 = {} &
        for n being Element of NAT holds
       (G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n))
   implies
       inf(rng (M*F)) = M.(F.0) - sup(rng (M*G));

theorem :: MEASURE3:14
     for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for F being Function of NAT,S holds
   ((for n being Element of NAT holds F.(n+1) c= F.n) &
   M.(F.0) <'+infty) implies
   (M.(meet rng F) = inf(rng (M*F)));

theorem :: MEASURE3:15
   for S being sigma_Field_Subset of X holds
   for M being Measure of S holds
   for T being N_Measure_fam of S holds
   for F being Sep_Sequence of S holds
   T = rng F implies
   SUM(M*F) <=' M.(union T);

theorem :: MEASURE3:16
    for S being sigma_Field_Subset of X holds
   for M being Measure of S holds
   for F being Sep_Sequence of S holds
   SUM(M*F) <=' M.(union rng F);

theorem :: MEASURE3:17
     for S being sigma_Field_Subset of X holds
   for M being Measure of S st
   (for F being Sep_Sequence of S holds
   M.(union rng F) <=' SUM(M*F)) holds
   M is sigma_Measure of S;

::
::                Completeness  of  sigma_additive  Measure
::

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
 canceled;

   pred M is_complete S means
:: MEASURE3:def 2
for A being Subset of X for B being set st B in S holds
     (A c= B & M.B = 0.) implies A in S;
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
   mode thin of M -> Subset of X means
:: MEASURE3:def 3
ex B being set st B in S & it c= B & M.B = 0.;
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
func COM(S,M) -> non empty Subset-Family of X means
:: MEASURE3:def 4
for A being set holds (A in it iff
   (ex B being set st B in S & ex C being thin of M st A = B \/ C));
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
   let A be Element of COM(S,M);
func MeasPart(A) -> non empty Subset-Family of X means
:: MEASURE3:def 5
for B being set holds (B in it iff (B in S & B c= A &
   A \ B is thin of M));
end;

theorem :: MEASURE3:18
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for F being Function of NAT,COM(S,M) holds
   ex G being Function of NAT,S st
   for n being Element of NAT holds G.n in MeasPart(F.n);

theorem :: MEASURE3:19
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for F being Function of NAT,COM(S,M) holds
   for G being Function of NAT,S holds
   (ex H being Function of NAT,bool X st
   for n being Element of NAT holds H.n = F.n \ G.n);

theorem :: MEASURE3:20
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for F being Function of NAT,bool X st
   (for n being Element of NAT holds F.n is thin of M) holds
   ex G being Function of NAT,S st
   (for n being Element of NAT holds
   F.n c= G.n & M.(G.n) = 0.);

theorem :: MEASURE3:21
   for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   for D being non empty Subset-Family of X holds
   (for A being set holds
   (A in D iff ex B being set st B in S & ex C being thin of M st A = B \/ C))
   implies D is sigma_Field_Subset of X;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
 cluster COM(S,M) -> sigma_Field_Subset-like compl-closed non empty;
end;

theorem :: MEASURE3:22
   for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       B1,B2 being set st B1 in S & B2 in S holds
   for C1,C2 being thin of M holds
   B1 \/ C1 = B2 \/ C2 implies M.B1 = M.B2;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let M be sigma_Measure of S;
func COM(M) -> sigma_Measure of COM(S,M) means
:: MEASURE3:def 6
for B being set st B in S
     for C being thin of M holds it.(B \/ C) = M.B;
end;

theorem :: MEASURE3:23
     for S being sigma_Field_Subset of X holds
   for M being sigma_Measure of S holds
   COM(M) is_complete COM(S,M);