Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Several Properties of the $\sigma$-additive Measure

by
Jozef Bialas

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));