The abstract of the Mizar article:

Several Properties of the $\sigma$-additive Measure

by

Jozef Bialas

Received July 3, 1991

MML identifier: MEASURE2

[ Mizar article, MML identifier index ]

environ

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


begin
::
::         Some useful theorems about measures and functions
::

 reserve X for set;

theorem :: MEASURE2:1
   for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       F being Function of NAT,S holds
   M*F is nonnegative;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   mode N_Measure_fam of S -> N_Sub_set_fam of X means
:: MEASURE2:def 1
 it c= S;
end;

canceled;

theorem :: MEASURE2:3
   for S being sigma_Field_Subset of X,
       T being N_Measure_fam of S holds
   meet T in S & union T in S;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let T be N_Measure_fam of S;
   redefine func meet T -> Element of S;

   redefine func union T -> Element of S;
end;

theorem :: MEASURE2:4
   for S being sigma_Field_Subset of X,
       N being Function of NAT,S holds
   ex F being Function of NAT,S st
   F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n;

theorem :: MEASURE2:5
   for S being sigma_Field_Subset of X,
       N being Function of NAT,S holds
   ex F being Function of NAT,S st
   F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n;

theorem :: MEASURE2:6
   for S being non empty Subset-Family of X,
       N,F being Function of NAT,S holds
    F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n)
   implies (for r being set for n being Nat holds (r in F.n iff
   ex k being Nat st (k <= n & r in N.k)));

theorem :: MEASURE2:7
   for S being non empty Subset-Family of X,
       N,F being Function of NAT,S holds
   (F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n)
   implies for n,m being Nat st n < m holds F.n c= F.m);

theorem :: MEASURE2:8
   for S being non empty Subset-Family of X,
       N, G, F being Function of NAT,S holds
   (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) &
   F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n))
   implies (for n,m being Nat st n <= m holds F.n c= G.m);

theorem :: MEASURE2:9
   for S being sigma_Field_Subset of X holds
   for N, G being Function of NAT,S holds
   ex F being Function of NAT,S st
   F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n;

theorem :: MEASURE2:10
     for S being sigma_Field_Subset of X holds
   for N being Function of NAT,S holds
   ex F being Function of NAT,S st
   F.0 = {} & for n being Element of NAT holds F.(n+1) = N.0 \ N.n;

theorem :: MEASURE2:11
   for S being sigma_Field_Subset of X holds
   for N, G, F being Function of NAT,S holds
   (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) &
   F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n))
   implies (for n,m being Nat st n < m holds F.n misses F.m);

canceled;

theorem :: MEASURE2:13
   for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       T being N_Measure_fam of S,
       F being Function of NAT,S st
   T = rng F holds M.(union T) <=' SUM(M*F);

theorem :: MEASURE2:14
   for S being sigma_Field_Subset of X,
       T being N_Measure_fam of S holds
   ex F being Function of NAT,S st T = rng F;

theorem :: MEASURE2:15
   for S being sigma_Field_Subset of X,
       N, F being Function of NAT,S st
   (F.0 = {} &
   for n being Element of NAT holds (F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n))
   holds
   for n being Element of NAT holds F.n c= F.(n+1);

theorem :: MEASURE2:16
     for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       T being N_Measure_fam of S holds
   (for A being set holds A in T implies A is measure_zero of M) implies
   union T is measure_zero of M;

theorem :: MEASURE2:17
   for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       T being N_Measure_fam of S st
   (ex A being set st A in T & A is measure_zero of M) holds
   meet T is measure_zero of M;

theorem :: MEASURE2:18
     for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       T being N_Measure_fam of S st
   (for A being set holds A in T implies A is measure_zero of M) holds
   meet T is measure_zero of M;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let IT be N_Measure_fam of S;
attr IT is non-decreasing means
:: MEASURE2:def 2
ex F being Function of NAT,S st
   IT = rng F & for n being Element of NAT holds F.n c= F.(n+1);
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
cluster non-decreasing N_Measure_fam of S;
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
   let IT be N_Measure_fam of S;
attr IT is non-increasing means
:: MEASURE2:def 3
  ex F being Function of NAT,S st
         (IT = rng F &
          for n being Element of NAT holds F.(n+1) c= F.n);
end;

definition
   let X be set;
   let S be sigma_Field_Subset of X;
cluster non-increasing N_Measure_fam of S;
end;

canceled 2;

theorem :: MEASURE2:21
     for S being sigma_Field_Subset of X,
       N,F being Function of NAT,S holds
   (F.0 = {} & for n being Element of NAT holds
   (F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n)) implies
   rng F is non-decreasing N_Measure_fam of S;

theorem :: MEASURE2:22
   for S being non empty Subset-Family of X,
       N being Function of NAT,S holds
   (for n being Element of NAT holds N.n c= N.(n+1))
   implies (for m,n being Nat st n < m holds N.n c= N.m);

theorem :: MEASURE2:23
   for S being sigma_Field_Subset of X,
       N,F being Function of NAT,S holds
   (F.0 = N.0 & for n being Element of NAT holds
   (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
   implies (for n,m being Nat st n < m holds F.n misses F.m);

theorem :: MEASURE2:24
   for S being sigma_Field_Subset of X,
       N,F being Function of NAT,S holds
   (F.0 = N.0 & for n being Element of NAT holds
   (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
   implies union rng F = union rng N;

theorem :: MEASURE2:25
   for S being sigma_Field_Subset of X,
       N,F being Function of NAT,S holds
   (F.0 = N.0 & for n being Element of NAT holds
   (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
   implies F is Sep_Sequence of S;

theorem :: MEASURE2:26
     for S being sigma_Field_Subset of X,
       N,F being Function of NAT,S holds
   (F.0 = N.0 & for n being Element of NAT holds
   (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
   implies (N.0 = F.0 & for n being Element of NAT holds
   N.(n+1) = F.(n+1) \/ N.n);

theorem :: MEASURE2:27
     for S being sigma_Field_Subset of X,
       M being sigma_Measure of S,
       F being Function of NAT,S st
   (for n being Element of NAT holds F.n c= F.(n+1)) holds
   M.(union rng F) = sup(rng (M*F));