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

by
Jozef Bialas

Copyright (c) 1992 Association of Mizar Users

MML identifier: MEASURE3
[ 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;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_1,
SUPINF_2, MEASURE1, MEASURE2, RELSET_1, PROB_2, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1;
schemes NAT_1, FUNCT_2, XBOOLE_0;

begin
::
::

reserve X for set;

theorem
for x being R_eal holds
(-infty <'x & x <'+infty) implies x is Real
proof
let x be R_eal;
assume
A1:-infty <'x & x <'+infty;
(x in REAL) or (x in {-infty,+infty}) by SUPINF_1:def 6,XBOOLE_0:def 2;
hence thesis by A1,TARSKI:def 2;
end;

theorem Th2:
for x being R_eal holds
((not x = -infty) & (not x = +infty)) implies x is Real
proof
let x be R_eal;
assume
A1:(not x = -infty) & (not x = +infty);
(x in REAL) or (x in {-infty,+infty}) by SUPINF_1:def 6,XBOOLE_0:def 2;
hence thesis by A1,TARSKI:def 2;
end;

theorem Th3:
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))
proof
let F1,F2 be Function of NAT,ExtREAL;
assume
A1:for n being Nat holds Ser(F1).n <=' Ser(F2).n;
A2:SUM(F1) = sup(rng Ser(F1)) by SUPINF_2:def 23;
A3:SUM(F2) = sup(rng Ser(F2)) by SUPINF_2:def 23;
for x being R_eal st x in rng Ser(F1) holds
(ex y being R_eal st y in rng Ser(F2) & x <=' y)
proof
let x be R_eal;
assume
A4:x in rng Ser(F1);
A5:dom Ser(F1) = NAT & dom Ser(F2) = NAT & rng Ser(F2) c= ExtREAL
by FUNCT_2:def 1;
then consider n being set such that
A6:n in NAT & x = Ser(F1).n by A4,FUNCT_1:def 5;
reconsider n as Nat by A6;
reconsider y = Ser(F2).n as R_eal;
take y;
thus thesis by A1,A5,A6,FUNCT_1:def 5;
end;
hence thesis by A2,A3,SUPINF_1:99;
end;

theorem
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)))
proof
let F1,F2 be Function of NAT,ExtREAL;
assume
A1:for n being Nat holds Ser(F1).n = Ser(F2).n;
then A2:for n being Nat holds Ser(F1).n <=' Ser(F2).n;
A3:for n being Nat holds Ser(F2).n <=' Ser(F1).n by A1;
A4:SUM(F1) <=' SUM(F2) by A2,Th3;
SUM(F2) <=' SUM(F1) by A3,Th3;
hence thesis by A4,SUPINF_1:22;
end;

::
::

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;
coherence
proof
A1:rng F is N_Sub_set_fam of X by MEASURE1:52;
rng F c= S by RELSET_1:12;
hence thesis by A1,MEASURE2:def 1;
end;
end;

theorem
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)
proof
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
let F be Function of NAT,S;
let A be Element of S;
assume
A1:(meet rng F c= A) & (for n being Element of NAT holds A c= F.n);
then A2:M.(meet rng F) <=' M.(A) by MEASURE1:62;
A c= meet rng F
proof
let x be set;
assume
A3:x in A;
for Y being set holds Y in rng F implies x in Y
proof
let Y be set;
assume
A4:Y in rng F;
dom F = NAT by FUNCT_2:def 1;
then ex n being set st n in NAT & Y = F.n by A4,FUNCT_1:def 5;
then A c= Y by A1;
hence thesis by A3;
end;
hence thesis by SETFAM_1:def 1;
end;
then M.(A) <=' M.(meet rng F) by MEASURE1:62;
hence thesis by A2,SUPINF_1:22;
end;

theorem Th6:
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
proof
let S be sigma_Field_Subset of X;
let G,F be Function of NAT,S;
assume
A1:G.0 = {} & for n being Element of NAT holds
(G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n);
A2:dom F = NAT & dom G = NAT & rng F c= S & rng G c= S
by FUNCT_2:def 1,RELSET_1:12;
thus union rng G c= F.0 \ meet rng F
proof
let A be set;
assume A in union rng G;
then consider Z being set such that
A3:A in Z & Z in rng G by TARSKI:def 4;
consider n being set such that
A4:n in NAT & Z = G.n by A2,A3,FUNCT_1:def 5;
reconsider n as Nat by A4;
consider k being Nat such that
A5:n = k + 1 by A1,A3,A4,NAT_1:22;
A6:  A in F.0 \ F.k by A1,A3,A4,A5;
then A7:A in F.0 & not A in F.k by XBOOLE_0:def 4;
set Y = F.k;
rng F <> {} & Y in rng F & not A in Y by A6,FUNCT_2:6,XBOOLE_0:def 4;
then not A in meet rng F by SETFAM_1:def 1;
hence thesis by A7,XBOOLE_0:def 4;
end;
let A be set;
assume A in F.0 \ meet rng F;
then A in F.0 & not A in meet rng F by XBOOLE_0:def 4;
then A in F.0 & ex Y being set st (Y in rng F & not A in Y)
by SETFAM_1:def 1;
then consider Y being set such that
A8:A in F.0 & Y in rng F & not A in Y;
consider n being set such that
A9:n in NAT & Y = F.n by A2,A8,FUNCT_1:def 5;
reconsider n as Nat by A9;
A in F.0 \ F.n by A8,A9,XBOOLE_0:def 4;
then A10:A in G.(n+1) by A1;
G.(n + 1) in rng G by FUNCT_2:6;
hence thesis by A10,TARSKI:def 4;
end;

theorem Th7:
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
proof
let S be sigma_Field_Subset of X;
let G,F be Function of NAT,S;
assume
A1:G.0 = {} & for n being Element of NAT holds
(G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n);
A2:for n being Element of NAT holds F.n c= F.0
proof
defpred P[Nat] means F.$1 c= F.0; A3: P[0]; A4:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A5:F.k c= F.0; F.(k+1) c= F.k by A1; hence thesis by A5,XBOOLE_1:1; end; thus for n being Nat holds P[n] from Ind(A3,A4); end; A6:union rng G = F.0 \ meet rng F by A1,Th6; A7:meet rng F c= F.0 proof let A be set; assume A8:A in meet rng F; A9:dom F = NAT by FUNCT_2:def 1; consider X being Element of rng F; A10:A in X by A8,SETFAM_1:def 1; ex n being set st n in NAT & F.n = X by A9,FUNCT_1:def 5; then X c= F.0 by A2; hence thesis by A10; end; F.0 /\ meet rng F = F.0 \ (F.0 \ meet rng F) by XBOOLE_1:48; hence thesis by A6,A7,XBOOLE_1:28; end; theorem Th8: 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) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let G,F be Function of NAT,S; assume A1: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); then A2:union rng G = F.0 \ meet rng F by Th6; A3:M.(F.0 \ union rng G) = M.(meet rng F) by A1,Th7; A4: not M.(F.0 \ meet rng F) = +infty proof assume A5:M.(F.0 \ meet rng F) = +infty; union rng G c= F.0 by A2,XBOOLE_1:36; hence thesis by A1,A2,A5,MEASURE1:62; end; M.(union rng G) <=' +infty by SUPINF_1:20; then A6:M.(union rng G) <'+infty by A2,A4,SUPINF_1:22; union rng G c= F.0 by A2,XBOOLE_1:36; hence thesis by A3,A6,MEASURE1:63; end; theorem Th9: 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) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let G,F be Function of NAT,S; assume A1: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); then A2:meet rng F = F.0 \ union rng G by Th7; A3:M.(F.0 \ meet rng F) = M.(union rng G) by A1,Th6; A4: not M.(F.0 \ union rng G) = +infty proof assume A5:M.(F.0 \ union rng G) = +infty; meet rng F c= F.0 by A2,XBOOLE_1:36; hence thesis by A1,A2,A5,MEASURE1:62; end; M.(meet rng F) <=' +infty by SUPINF_1:20; then A6:M.(meet rng F) <'+infty by A2,A4,SUPINF_1:22; meet rng F c= F.0 by A2,XBOOLE_1:36; hence thesis by A3,A6,MEASURE1:63; end; theorem 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)) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let G,F be Function of NAT,S; assume A1: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); then for n being Element of NAT holds G.n c= G.(n+1) by MEASURE2:15; then M.(union rng G) = sup(rng (M*G)) by MEASURE2:27; hence thesis by A1,Th8; end; theorem Th11: 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 proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let G,F be Function of NAT,S; assume A1: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); reconsider P = {} as Element of S by MEASURE1:45; P c= F.0 by XBOOLE_1:2; then M.P <=' M.(F.0) by MEASURE1:62; then A2:0. <=' M.(F.0) by MEASURE1:def 11; ex x being R_eal st x in rng(M*F) & x = M.(F.0) proof A3:dom (M*F) = NAT by FUNCT_2:def 1; take (M*F).0; thus thesis by A3,FUNCT_1:22,FUNCT_2:6; end; then A4:inf(rng(M*F)) <=' M.(F.0) by SUPINF_1:79; for x being R_eal holds x in rng(M*F) implies 0.<=' x proof let x be R_eal; assume A5:x in rng(M*F); dom (M*F) = NAT by FUNCT_2:def 1; then A6: ex n being set st n in NAT & (M*F).n = x by A5,FUNCT_1:def 5; (M*F) is nonnegative by MEASURE2:1; hence thesis by A6,SUPINF_2:58; end; then 0. is minorant of rng(M*F) by SUPINF_1:def 10; then A7:not inf(rng(M*F)) = -infty by SUPINF_1:def 17,SUPINF_2:19; for x being R_eal holds x in rng(M*G) implies x <=' M.(F.0) proof let x be R_eal; assume A8:x in rng(M*G); A9:dom (M*G) = NAT by FUNCT_2:def 1; then consider n being set such that A10:n in NAT & (M*G).n = x by A8,FUNCT_1:def 5; reconsider n as Nat by A10; A11:x = M.(G.n) by A9,A10,FUNCT_1:22; A12:n = 0 implies x <=' M.(F.0) proof assume n = 0; then G.n c= F.0 by A1,XBOOLE_1:2; hence thesis by A11,MEASURE1:62; end; (ex k being Nat st n = k + 1) implies x <=' M.(F.0) proof given k being Nat such that A13:n = k + 1; G.n = F.0 \ F.k by A1,A13; then G.n c= F.0 by XBOOLE_1:36; hence thesis by A11,MEASURE1:62; end; hence thesis by A12,NAT_1:22; end; then A14: M.(F.0) is majorant of rng(M*G) by SUPINF_1:def 9; A15:0. <=' sup(rng(M*G)) proof A16:for x being R_eal holds x in rng(M*G) implies 0.<=' x proof let x be R_eal; assume A17:x in rng(M*G); dom (M*G) = NAT by FUNCT_2:def 1; then A18: ex n being set st n in NAT & (M*G).n = x by A17,FUNCT_1: def 5; (M*G) is nonnegative by MEASURE2:1; hence thesis by A18,SUPINF_2:58; end; A19:(M*G).0 in rng(M*G) by FUNCT_2:6; set x = (M*G).0; A20:0. <=' x by A16,A19; x <=' sup rng(M*G) by A19,SUPINF_1:76; hence thesis by A20,SUPINF_1:29; end; not sup(rng(M*G)) = +infty by A1,A14,SUPINF_1:def 16; hence thesis by A1,A2,A4,A7,A15,Th2,SUPINF_2:19; end; theorem Th12: 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)) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let G,F be Function of NAT,S; assume A1: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); then A2:for n being Element of NAT holds G.n c= G.(n+1) by MEASURE2:15; reconsider P = {} as Element of S by MEASURE1:45; P c= F.0 by XBOOLE_1:2; then M.P <=' M.(F.0) by MEASURE1:62; then A3:0. <=' M.(F.0) by MEASURE1:def 11; set l = M.(F.0) - inf(rng (M*F)); A4:l is majorant of rng (M*G) proof for x being R_eal holds x in rng (M*G) implies x <=' l proof let x be R_eal; assume A5:x in rng (M*G); A6:dom (M*F) = NAT & dom (M*G) = NAT by FUNCT_2:def 1; then consider n being set such that A7:n in NAT & (M*G).n = x by A5,FUNCT_1:def 5; reconsider n as Nat by A7; A8: M*G is nonnegative by MEASURE2:1; then A9:0. <=' x by A7,SUPINF_2:58; A10:x = M.(G.n) by A6,A7,FUNCT_1:22; A11:n = 0 implies G.n c= F.0 by A1,XBOOLE_1:2; A12: (ex k being Nat st n = k + 1) implies G.n c= F.0 proof given k being Nat such that A13:n = k + 1; G.n = F.0 \ F.k by A1,A13; hence thesis by XBOOLE_1:36; end; then A14: x <=' M.(F.0) by A10,A11,MEASURE1:62,NAT_1:22; A15:not x = +infty by A1,A10,A11,A12,MEASURE1:62,NAT_1:22; A16:not x = -infty by A7,A8,SUPINF_2:19,58; A17:x is Real by A9,A15,Th2,SUPINF_2:19; A18:inf(rng (M*F)) <=' M.(F.0) - x proof M.(G.n) <'+infty by A10,A17,SUPINF_1:31; then A19:M.(F.0) - x = M.(F.0 \ G.n) by A10,A11,A12,MEASURE1:63, NAT_1:22; M.(F.0 \ G.n) in rng (M*F) proof A20:n = 0 implies M.(F.0 \ G.n) in rng (M*F) proof assume A21: n = 0; M.(F.0) = (M*F).0 by A6,FUNCT_1:22; hence thesis by A1,A21,FUNCT_2:6; end; (ex k being Nat st n = k + 1) implies M.(F.0 \ G.n) in rng (M*F) proof given k being Nat such that A22:n = k + 1; for n being Element of NAT holds F.n c= F.0 proof defpred P[Nat] means F.$1 c= F.0;
A23: P[0];
A24:for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A25:F.k c= F.0;
F.(k+1) c= F.k by A1;
hence thesis by A25,XBOOLE_1:1;
end;
thus for n being Nat holds P[n] from Ind(A23,A24);
end;
then A26:F.k c= F.0;
A27:                 F.0 \ G.n = F.0 \ ( F.0 \ F.k) by A1,A22
.= F.0 /\ F.k by XBOOLE_1:48
.= F.k by A26,XBOOLE_1:28;
M.(F.k) = (M*F).k by A6,FUNCT_1:22;
hence thesis by A27,FUNCT_2:6;
end;
hence thesis by A20,NAT_1:22;
end;
hence thesis by A19,SUPINF_1:79;
end;
A28:M.(F.0) is Real by A1,Th11;
A29:inf(rng(M*F)) is Real by A1,Th11;
then consider a,b,c being Real such that
A30:a = M.(F.0) & b = x & c = inf(rng (M*F)) by A17,A28;
M.(F.0) - x = a - b by A30,SUPINF_2:5;
then (M.(F.0) - x) + x = (a - b) + b by A30,SUPINF_2:1
.= (a + -b) + b by XCMPLX_0:def 8
.= a + (-b + b) by XCMPLX_1:1
.= a + 0 by XCMPLX_0:def 6
.= M.(F.0) by A30;
then A31:inf(rng (M*F)) + x <=' M.(F.0) by A1,A14,A16,A18,SUPINF_2:14;
A32:        not ((M.(F.0) = +infty & inf(rng (M*F)) = +infty) or
(M.(F.0) = -infty & inf(rng (M*F)) = -infty)) &
not ((inf(rng (M*F)) + x = +infty & inf(rng (M*F)) = +infty) or
(inf(rng (M*F)) + x = -infty & inf(rng (M*F)) = -infty))
by A29,SUPINF_1:2,6;
inf(rng (M*F)) + x = c + b by A30,SUPINF_2:1;
then inf(rng (M*F)) + x - inf(rng (M*F)) = b + c - c by A30,
SUPINF_2:5
.= b + c + -c by XCMPLX_0:def 8
.= b + (c + -c) by XCMPLX_1:1
.= b + 0 by XCMPLX_0:def 6
.= x by A30;
hence thesis by A31,A32,SUPINF_2:15;
end;
hence thesis by SUPINF_1:def 9;
end;
for y being R_eal holds y is majorant of rng (M*G) implies l <=' y
proof
let y be R_eal;
assume
A33:y is majorant of rng (M*G);
l <=' y
proof
set Q = union rng G;
sup(rng(M*G)) = M.(Q) by A2,MEASURE2:27;
then A34:M.Q <=' y by A33,SUPINF_1:def 16;
l <=' M.Q
proof
A35:        M.(F.0) - M.(meet rng F) = M.(union rng G) by A1,Th9;
M.(F.0) - inf(rng (M*F)) <=' M.(union rng G)
proof
for x being R_eal holds
x in rng (M*F) implies M.(meet rng F) <=' x
proof
let x be R_eal;
assume
A36:x in rng (M*F);
A37:dom (M*F) = NAT by FUNCT_2:def 1;
then consider n being set such that
A38:n in NAT & (M*F).n = x by A36,FUNCT_1:def 5;
reconsider n as Nat by A38;
A39:x = M.(F.n) by A37,A38,FUNCT_1:22;
meet rng F c= F.n
proof
F.n in rng F by FUNCT_2:6;
hence thesis by SETFAM_1:4;
end;
hence thesis by A39,MEASURE1:62;
end;
then M.(meet rng F) is minorant of rng (M*F) by SUPINF_1:def 10
;
then M.(meet rng F) <=' inf(rng (M*F)) by SUPINF_1:def 17;
hence thesis by A1,A3,A35,SUPINF_2:15,19;
end;
hence thesis;
end;
hence thesis by A34,SUPINF_1:29;
end;
hence thesis;
end;
hence thesis by A4,SUPINF_1:def 16;
end;

theorem Th13:
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))
proof
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
let G,F be Function of NAT,S;
assume
A1: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);
set l = M.(F.0) - sup(rng (M*G));
A2:l is minorant of rng (M*F)
proof
for x being R_eal holds x in rng (M*F) implies l <=' x
proof
let x be R_eal;
assume
A3:x in rng (M*F);
l <=' x
proof
not x = +infty implies l <='x
proof
assume
A4:not x = +infty;
A5:dom (M*F) = NAT & dom (M*G) = NAT by FUNCT_2:def 1;
then consider n being set such that
A6:n in NAT & (M*F).n = x by A3,FUNCT_1:def 5;
reconsider n as Nat by A6;
M*F is nonnegative by MEASURE2:1;
then A7:0. <=' x by A6,SUPINF_2:58;
A8:M.(F.0) - x <=' sup(rng (M*G))
proof
for n being Element of NAT holds F.n c= F.0
proof
defpred P[Nat] means F.$1 c= F.0; A9: P[0]; A10:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A11:F.k c= F.0; F.(k+1) c= F.k by A1; hence thesis by A11,XBOOLE_1:1; end; thus for k being Nat holds P[k] from Ind(A9,A10); end; then A12:F.n c= F.0; then M.(F.n) <=' M.(F.0) by MEASURE1:62; then A13:M.(F.n) <'+infty by A1,SUPINF_1:29; A14:M.(F.0) - x = M.(F.0) - M.(F.n) by A5,A6,FUNCT_1:22 .= M.(F.0 \ F.n) by A12,A13,MEASURE1:63 .= M.(G.(n+1)) by A1; set k = n + 1; A15:M.(F.0) - x = (M*G).k by A5,A14,FUNCT_1:22; (M*G).k in rng (M*G) by FUNCT_2:6; hence thesis by A15,SUPINF_1:76; end; A16:M.(F.0) is Real by A1,Th11; A17:x is Real by A4,A7,Th2,SUPINF_2:19; A18:sup(rng(M*G)) is Real by A1,Th11; then consider a,b,c being Real such that A19:a = M.(F.0) & b = x & c = sup(rng (M*G)) by A16,A17; M.(F.0) - x = a - b by A19,SUPINF_2:5; then (M.(F.0) - x) + x = (a - b) + b by A19,SUPINF_2:1 .= (a + -b) + b by XCMPLX_0:def 8 .= a + (-b + b) by XCMPLX_1:1 .= a + 0 by XCMPLX_0:def 6 .= M.(F.0) by A19; then A20:M.(F.0) <=' sup(rng (M*G)) + x by A4,A7,A8,SUPINF_2:14,19; A21: not ((M.(F.0) = +infty & sup(rng (M*G)) = +infty) or (M.(F.0) = -infty & sup(rng (M*G)) = -infty)) & not ((sup(rng (M*G)) + x = +infty & sup(rng (M*G)) = +infty) or (sup(rng (M*G)) + x = -infty & sup(rng (M*G)) = -infty )) by A18,SUPINF_1:2,6; sup(rng (M*G)) + x = c + b by A19,SUPINF_2:1; then sup(rng (M*G)) + x - sup(rng (M*G)) = b + c - c by A19,SUPINF_2 :5 .= b + c + -c by XCMPLX_0:def 8 .= b + (c + -c) by XCMPLX_1:1 .= b + 0 by XCMPLX_0:def 6 .= x by A19; hence thesis by A20,A21,SUPINF_2:15; end; hence thesis by SUPINF_1:20; end; hence thesis; end; hence thesis by SUPINF_1:def 10; end; for y being R_eal holds (y is minorant of rng (M*F) implies y <=' l) proof let y be R_eal; assume A22:y is minorant of rng (M*F); A23: sup(rng (M*G)) = M.(F.0) - inf(rng (M*F)) by A1,Th12; sup(rng (M*G)) is Real & M.(F.0) is Real & inf(rng (M*F)) is Real by A1,Th11; then consider a,b,c being Real such that A24:a = sup(rng (M*G)) & b = M.(F.0) & c = inf(rng (M*F)); consider s,t,r being R_eal such that A25:s = sup(rng (M*G)) & t = M.(F.0) - inf(rng (M*F)) & r = inf(rng (M*F)); M.(F.0) - inf(rng (M*F)) = b - c by A24,SUPINF_2:5; then A26: M.(F.0) - inf(rng (M*F)) + r = b - c + c by A24,A25,SUPINF_2:1 .= b + -c + c by XCMPLX_0:def 8 .= b + (-c + c) by XCMPLX_1:1 .= b + 0 by XCMPLX_0:def 6 .= M.(F.0) by A24; sup(rng (M*G)) + inf(rng (M*F)) = a + c by A24,SUPINF_2:1; then sup(rng (M*G)) + inf(rng (M*F)) - sup(rng (M*G)) = c + a - a by A24,SUPINF_2:5 .= c + a + -a by XCMPLX_0:def 8 .= c + (a + -a) by XCMPLX_1:1 .= c + 0 by XCMPLX_0:def 6 .= inf(rng (M*F)) by A24; hence thesis by A22,A23,A25,A26,SUPINF_1:def 17; end; hence thesis by A2,SUPINF_1:def 17; end; theorem 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))) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let F be Function of NAT,S; assume A1:(for n being Element of NAT holds F.(n+1) c= F.n) & M.(F.0) <'+infty; consider G being Function of NAT,S such that A2:G.0 = {} & for n being Element of NAT holds G.(n+1) = F.0 \ F.n by MEASURE2:10; for n being Element of NAT holds G.n c= G.(n+1) by A1,A2,MEASURE2:15; then A3:M.(union rng G) = sup(rng (M*G)) by MEASURE2:27; A4:union rng G = F.0 \ meet rng F by A1,A2,Th6; A5:M.(F.0 \ union rng G) = M.(meet rng F) by A1,A2,Th7; for A being Element of S holds A = union rng G implies M.(meet rng F) = M.(F.0) - M.A proof let A be Element of S; assume A6:A = union rng G; A7: not M.(F.0 \ meet rng F) = +infty proof assume A8:M.(F.0 \ meet rng F) = +infty; A c= F.0 by A4,A6,XBOOLE_1:36; hence thesis by A1,A4,A6,A8,MEASURE1:62; end; M.A <=' +infty by SUPINF_1:20; then A9:M.A <'+infty by A4,A6,A7,SUPINF_1:22; A c= F.0 by A4,A6,XBOOLE_1:36; hence thesis by A5,A6,A9,MEASURE1:63; end; then M.(meet rng F) = M.(F.0) - sup(rng (M*G)) by A3; hence thesis by A1,A2,Th13; end; theorem Th15: 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) proof let S be sigma_Field_Subset of X; let M be Measure of S; let T be N_Measure_fam of S; let F be Sep_Sequence of S; assume A1:T = rng F; union T is Subset of X & {} is Subset of X by XBOOLE_1:2; then consider H being Function of NAT,bool X such that A2:(rng H = {union T,{}}) & (H.0 = union T) & (for n being Nat st 0 < n holds H.n = {}) by MEASURE1:40; rng H c= S proof let a be set; assume a in rng H; then a = union T or a = {} by A2,TARSKI:def 2; hence thesis by MEASURE1:45; end; then reconsider H as Function of NAT,S by FUNCT_2:8; M is nonnegative by MEASURE1:def 5; then A3:M*F is nonnegative & M*H is nonnegative by MEASURE1:54; consider G being Function of NAT,S such that A4:G.0 = F.0 & for n being Element of NAT holds G.(n+1) = F.(n+1) \/ G.n by MEASURE2:5; A5:for n being Nat holds G.n /\ F.(n+1) = {} proof let n be Nat; A6:for n being Nat holds for k being Nat st n < k holds G.n /\ F.k = {} proof defpred P[Nat] means for k being Nat holds$1 < k implies G.$1 /\ F.k = {}; A7: P[0] proof let k be Nat; assume 0 < k; then F.0 misses F.k by PROB_2:def 3; hence thesis by A4,XBOOLE_0:def 7; end; A8:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A9:for k being Nat st n < k holds G.n /\ F.k = {}; let k be Nat; assume A10:n+1 < k; A11:G.(n+1) /\ F.k = (F.(n+1) \/ G.n) /\ F.k by A4 .= (F.(n+1) /\ F.k) \/ (G.n /\ F.k) by XBOOLE_1:23; A12: n < k by A10,NAT_1:38; F.(n+1) misses F.k by A10,PROB_2:def 3; then F.(n+1) /\ F.k = {} by XBOOLE_0:def 7; hence thesis by A9,A11,A12; end; thus for n being Nat holds P[n] from Ind(A7,A8); end; n < n + 1 by NAT_1:38; hence thesis by A6; end; A13:Ser(M*F).0 = (M*F).0 by SUPINF_2:63; defpred P[Nat] means Ser(M*F).$1 = M.(G.$1); A14:dom F = NAT & dom (M*F) = NAT by FUNCT_2:def 1; then A15: P[0] by A4,A13,FUNCT_1:22; A16:for n being Nat holds Ser(M*F).n = M.(G.n) proof A17:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume Ser(M*F).k = M.(G.k); then A18:Ser(M*F).(k+1) = M.(G.k) + (M*F).(k+1) by SUPINF_2:63; G.k /\ F.(k+1) = {} by A5; then A19: G.k misses F.(k+1) by XBOOLE_0:def 7; Ser(M*F).(k+1) = M.(G.k) + M.(F.(k+1)) by A14,A18,FUNCT_1:22 .= M.(F.(k+1) \/ G.k) by A19,MEASURE1:def 5 .= M.(G.(k+1)) by A4; hence thesis; end; thus for n being Nat holds P[n] from Ind(A15,A17); end; A20:for n being Nat holds G.n c= union T proof defpred P[Nat] means G.$1 c= union T;
G.0 in rng F by A4,FUNCT_2:6;
then A21: P[0] by A1,ZFMISC_1:92;
A22:for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A23:G.n c= union T;
A24:G.(n+1) = F.(n+1) \/ G.n by A4;
F.(n+1) in T by A1,FUNCT_2:6;
then F.(n+1) c= union T by ZFMISC_1:92;
hence thesis by A23,A24,XBOOLE_1:8;
end;
thus for n being Nat holds P[n] from Ind(A21,A22);
end;
defpred P[Nat] means Ser(M*H).$1 = M.(union T); A25: P[0] proof A26:Ser(M*H).0 = (M*H).0 by SUPINF_2:63; dom (M*H) = NAT by FUNCT_2:def 1; hence thesis by A2,A26,FUNCT_1:22; end; A27:for n being Nat holds Ser(M*H).n = M.(union T) proof A28:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume Ser(M*H).n = M.(union T); then A29:Ser(M*H).(n+1) = M.(union T) + (M*H).(n+1) by SUPINF_2:63; 0 <= n by NAT_1:18; then 0 < n + 1 by NAT_1:38; then A30:H.(n+1) = {} by A2; dom (M*H) = NAT by FUNCT_2:def 1; then (M*H).(n+1) = M.({}) by A30,FUNCT_1:22; then (M*H).(n+1) = 0. by MEASURE1:def 5; hence thesis by A29,SUPINF_2:18; end; thus for n being Nat holds P[n] from Ind(A25,A28); end; A31: for n being Nat holds Ser(M*F).n <=' Ser(M*H).n proof let n be Nat; A32:Ser(M*F).n = M.(G.n) by A16; G.n c= union T by A20; then Ser(M*F).n <=' M.(union T) by A32,MEASURE1:25; hence thesis by A27; end; for r being Nat st 1 <= r holds (M*H).r = 0. proof let r be Nat; assume 1 <= r; then 0 + 1 <= r; then 0 < r by NAT_1:38; then A33:H.r = {} by A2; dom (M*H) = NAT by FUNCT_2:def 1; then (M*H).r = M.({}) by A33,FUNCT_1:22; hence thesis by MEASURE1:def 5; end; then SUM(M*H) = Ser(M*H).1 by A3,SUPINF_2:67; then SUM(M*H) = M.(union T) by A27; hence thesis by A31,Th3; end; theorem 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) by Th15; theorem 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 proof let S be sigma_Field_Subset of X; let M be Measure of S; assume A1:for F being Sep_Sequence of S holds M.(union rng F) <=' SUM(M*F); A2:for F being Sep_Sequence of S holds SUM(M*F) = M.(union rng F) proof let F be Sep_Sequence of S; A3:M.(union rng F) <=' SUM(M*F) by A1; SUM(M*F) <=' M.(union rng F) by Th15; hence thesis by A3,SUPINF_1:22; end; M is nonnegative & M.{} = 0. by MEASURE1:def 5; hence thesis by A2,MEASURE1:def 11; end; :: :: 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 :Def2: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 :Def3:ex B being set st B in S & it c= B & M.B = 0.; existence proof reconsider A = {} as Subset of X by XBOOLE_1:2; take A; take B={}; thus B in S by MEASURE1:45; thus A c= B; thus thesis by MEASURE1:def 11; end; 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 :Def4: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)); existence proof defpred P[set] means for A being set st A =$1 holds
ex B being set st B in S & ex C being thin of M st A = B \/ C;
consider D being set such that
A1:for y being set holds y in D iff y in bool X & P[y] from Separation;
A2:D c= bool X
proof
let x be set; assume x in D;
hence x in bool X by A1;
end;
A3: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)))
proof
let A be set;
A4:A in D iff (A in bool X &
for y being set holds (y = A implies
(ex B being set st (B in S & ex C being thin of M st y = B \/ C))))
by A1;
(ex B being set st (B in S & ex C being thin of M st A = B \/ C))
implies A in D
proof
assume
A5:ex B being set st (B in S & ex C being thin of M st A = B \/ C);
then consider B being set such that
A6:B in S & ex C being thin of M st A = B \/ C;
A c= X by A6,XBOOLE_1:8;
hence thesis by A4,A5;
end;
hence thesis by A1;
end;
A7:{} is Subset of X by XBOOLE_1:2;
ex B being set st B in S & {} c= B & M.B = 0.
proof
{} in S by MEASURE1:45;
then consider B being set such that
A8:B = {} & B in S;
take B;
thus thesis by A8,MEASURE1:def 11;
end;
then A9:{} is thin of M by A7,Def3;
A10:{} c= X by XBOOLE_1:2;
for A being set st A = {} holds
ex B being set st B in S & ex C being thin of M st A = B \/ C
proof
let A be set;
assume
A11:A = {};
{} in S by MEASURE1:45;
then consider B being set such that
A12:B = {} & B in S;
consider C being thin of M such that
A13:C = {} by A9;
A = B \/ C by A11,A12,A13;
hence thesis by A12;
end;
then reconsider D as non empty Subset-Family of X by A1,A2,A10,SETFAM_1:def
7;
take D;
thus thesis by A3;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of X such that
A14:for A being set holds (A in D1 iff
(ex B being set st (B in S & ex C being thin of M st A = B \/ C))) and
A15:for A being set holds (A in D2 iff
(ex B being set st (B in S & ex C being thin of M st A = B \/ C)));
for A being set holds A in D1 iff A in D2
proof
let A be set;
thus A in D1 implies A in D2
proof
assume A in D1;
then ex B being set st (B in S & ex C being thin of M st A = B \/ C)
by A14;
hence thesis by A15;
end;
assume A in D2;
then ex B being set st (B in S & ex C being thin of M st A = B \/ C) by
A15;
hence thesis by A14;
end;
hence thesis by TARSKI:2;
end;
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
:Def5:for B being set holds (B in it iff (B in S & B c= A &
A \ B is thin of M));
existence
proof
defpred P[set] means
for t being set holds (t = $1 implies (t in S & t c= A & A \ t is thin of M)); consider D being set such that A1:for t being set holds (t in D iff t in bool X & P[t]) from Separation; A2:for B being set holds (B in D iff B in S & B c= A & A \ B is thin of M) proof let B be set; B in S & B c= A & A \ B is thin of M implies B in D proof assume A3:B in S & B c= A & A \ B is thin of M; then for t being set holds t = B implies (t in S & t c= A & A \ t is thin of M); hence thesis by A1,A3; end; hence thesis by A1; end; D <> {} proof consider B being set such that A4:B in S & ex C being thin of M st A = B \/ C by Def4; consider C being thin of M such that A5:A = B \/ C by A4; consider E being set such that A6:E in S & C c= E & M.E = 0. by Def3; A \ B = C \ B by A5,XBOOLE_1:40; then A7: A \ B c= C by XBOOLE_1:36; then A8:A \ B c= E by A6,XBOOLE_1:1; A \ B c= X by A7,XBOOLE_1:1; then A9:A \ B is thin of M by A6,A8,Def3; B c= A by A5,XBOOLE_1:7; hence thesis by A2,A4,A9; end; then consider x being set such that A10: x in D by XBOOLE_0:def 1; D c= bool X proof let B be set; assume B in D; then B in S by A2; hence thesis; end; then reconsider D as non empty Subset-Family of X by A10,SETFAM_1:def 7; take D; thus thesis by A2; end; uniqueness proof let D1,D2 be non empty Subset-Family of X such that A11:for B being set holds B in D1 iff (B in S & B c= A & A \ B is thin of M) and A12:for B being set holds B in D2 iff (B in S & B c= A & A \ B is thin of M); for B being set holds B in D1 iff B in D2 proof let B be set; thus B in D1 implies B in D2 proof assume B in D1; then B in S & B c= A & A \ B is thin of M by A11; hence thesis by A12; end; assume B in D2; then B in S & B c= A & A \ B is thin of M by A12; hence thesis by A11; end; hence thesis by TARSKI:2; end; end; theorem Th18: 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) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let F be Function of NAT,COM(S,M); defpred P[Element of NAT, set] means for n being Element of NAT for y being set holds (n =$1 & y = $2 implies y in MeasPart(F.n)); A1: for t being Element of NAT ex A being Element of S st P[t,A] proof let t be Element of NAT; consider A being Element of MeasPart(F.t); reconsider A as Element of S by Def5; take A; thus thesis; end; ex G being Function of NAT,S st for t being Element of NAT holds P[t,G.t] from FuncExD(A1); then consider G being Function of NAT,S such that A2: for t being Element of NAT holds for n being Element of NAT for y being set holds (n = t & y = G.t implies y in MeasPart(F.n)); take G; thus thesis by A2; end; theorem Th19: 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) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let F be Function of NAT,COM(S,M); let G be Function of NAT,S; defpred P[Element of NAT, set] means for n being Element of NAT for y being set holds (n =$1 & y = $2 implies y = F.n \ G.n); A1: for t being Element of NAT ex A being Element of bool X st P[t,A] proof let t be Element of NAT; A2: F.t is Element of COM(S,M); F.t \ G.t c= F.t by XBOOLE_1:36; then reconsider A = F.t \ G.t as Element of bool X by A2,XBOOLE_1:1; take A; thus thesis; end; ex H being Function of NAT,bool X st for t being Element of NAT holds P[t,H.t] from FuncExD(A1); then consider H being Function of NAT,bool X such that A3: for t being Element of NAT holds for n being Element of NAT for y being set holds (n = t & y = H.t implies y = F.n \ G.n); take H; thus thesis by A3; end; theorem Th20: 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.) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let F be Function of NAT,bool X; assume A1:for n being Element of NAT holds F.n is thin of M; defpred P[Element of NAT, set] means for n being Element of NAT for y being set holds (n =$1 & y = $2 implies y in S & F.n c= y & M.y = 0.); A2: for t being Element of NAT ex A being Element of S st P[t,A] proof let t be Element of NAT; F.t is thin of M by A1; then consider A being set such that A3:A in S & F.t c= A & M.A = 0. by Def3; reconsider A as Element of S by A3; take A; thus thesis by A3; end; ex G being Function of NAT,S st for t being Element of NAT holds P[t,G.t] from FuncExD(A2); then consider G being Function of NAT,S such that A4: for t being Element of NAT holds for n being Element of NAT for y being set holds (n = t & y = G.t implies y in S & F.n c= y & M.y = 0.); take G; thus thesis by A4; end; Lm1: for P,G,C being set holds C c= G implies P \ C = (P \ G) \/ (P /\ (G \ C)) proof let P,G,C be set; assume A1:C c= G; thus P \ C c= (P \ G) \/ (P /\ (G \ C)) proof let x be set; assume x in P \ C; then (x in P & not x in G) or (x in P & (x in G & not x in C)) by XBOOLE_0:def 4; then x in P \ G or (x in P & x in G \ C) by XBOOLE_0:def 4; then x in P \ G or x in P /\ (G \ C) by XBOOLE_0:def 3; hence thesis by XBOOLE_0:def 2; end; let x be set; assume x in (P \ G) \/ (P /\ (G \ C)); then x in P \ G or x in (P /\ (G \ C)) by XBOOLE_0:def 2; then x in P \ G or (x in P & x in (G \ C)) by XBOOLE_0:def 3; then x in P & not x in C by A1,XBOOLE_0:def 4; hence thesis by XBOOLE_0:def 4; end; theorem Th21: 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 proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let D be non empty Subset-Family of X; assume A1: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); A2:for A being set holds A in D implies X\A in D proof let A be set; assume A3:A in D; ex Q being set st Q in S & ex W being thin of M st X \ A = Q \/ W proof consider B being set such that A4:B in S & ex C being thin of M st A = B \/ C by A1,A3; consider C being thin of M such that A5:A = B \/ C by A4; consider G being set such that A6:G in S & C c= G & M.G = 0. by Def3; set P = X \ B; A7:X \ B in S by A4,MEASURE1:def 3; A8:X \ A = P \ C by A5,XBOOLE_1:41; set Q = P \ G; A9:ex W being thin of M st X \ A = Q \/ W proof set W = P /\ (G \ C); A10:ex R being set st (R in S & W c= R & M.R = 0.) proof take G; A11:W c= G \ C by XBOOLE_1:17; G \ C c= G by XBOOLE_1:36; hence thesis by A6,A11,XBOOLE_1:1; end; W c= P by XBOOLE_1:17; then reconsider W as Subset of X by A7,XBOOLE_1:1; reconsider W as thin of M by A10,Def3; take W; thus thesis by A6,A8,Lm1; end; take Q; thus thesis by A6,A7,A9,MEASURE1:47; end; hence thesis by A1; end; for K being N_Sub_set_fam of X holds K c= D implies union K in D proof let K be N_Sub_set_fam of X; assume A12:K c= D; consider F being Function of NAT,bool X such that A13:K = rng F by SUPINF_2:def 14; A14:dom F = NAT by FUNCT_2:def 1; A15:for n being Nat holds F.n in D proof let n be Nat; F.n in K by A13,FUNCT_2:6; hence thesis by A12; end; A16:for n being Nat holds ex B being set st B in S & ex C being thin of M st F.n = B \/ C proof let n be Nat; F.n in D by A15; hence thesis by A1; end; for n being Nat holds F.n in COM(S,M) proof let n be Nat; ex B being set st (B in S & ex C being thin of M st F.n = B \/ C) by A16; hence thesis by Def4; end; then for n being set st n in NAT holds F.n in COM(S,M); then reconsider F as Function of NAT,COM(S,M) by A14,FUNCT_2:5; consider G being Function of NAT,S such that A17:for n being Element of NAT holds G.n in MeasPart(F.n) by Th18; A18:for n being Element of NAT holds G.n in S & G.n c= F.n & F.n \ G.n is thin of M proof let n be Element of NAT; G.n in MeasPart(F.n) by A17; hence thesis by Def5; end; consider H be Function of NAT,bool X such that A19:for n being Element of NAT holds (H.n = F.n \ G.n) by Th19; for n being Element of NAT holds H.n is thin of M proof let n be Element of NAT; F.n \ G.n is thin of M by A18; hence thesis by A19; end; then consider L being Function of NAT,S such that A20:for n being Element of NAT holds H.n c= L.n & M.(L.n) = 0. by Th20; ex B being set st B in S & ex C being thin of M st union K = B \/ C proof set B = union rng G; A21:union rng G c= union rng F proof let x be set; assume x in union rng G; then consider Z being set such that A22:x in Z & Z in rng G by TARSKI:def 4; dom G = NAT by FUNCT_2:def 1; then consider n being set such that A23:n in NAT & Z = G.n by A22,FUNCT_1:def 5; reconsider n as Element of NAT by A23; set P = F.n; A24: G.n c= P by A18; ex P being set st P in rng F & x in P proof take P; thus thesis by A14,A22,A23,A24,FUNCT_1:def 5; end; hence thesis by TARSKI:def 4; end; A25:ex C being thin of M st union K = B \/ C proof set C = union K \ B; A26:union K = C \/ union rng F /\ union rng G by A13,XBOOLE_1:51 .= B \/ C by A21,XBOOLE_1:28; reconsider C as Subset of X; C is thin of M proof A27:C c= union rng H proof let x be set; assume x in C; then A28:x in union rng F & not x in union rng G by A13,XBOOLE_0: def 4; then consider Z being set such that A29:x in Z & Z in rng F by TARSKI:def 4; consider n being set such that A30:n in NAT & Z = F.n by A14,A29,FUNCT_1:def 5; reconsider n as Element of NAT by A30; not x in G.n proof assume A31:x in G.n; dom G = NAT by FUNCT_2:def 1; then G.n in rng G by FUNCT_1:def 5; hence thesis by A28,A31,TARSKI:def 4; end; then A32: x in F.n \ G.n by A29,A30,XBOOLE_0:def 4; ex Z being set st x in Z & Z in rng H proof A33: dom H = NAT by FUNCT_2:def 1; take H.n; thus thesis by A19,A32,A33,FUNCT_1:def 5; end; hence thesis by TARSKI:def 4; end; union rng H c= union rng L proof let x be set; assume x in union rng H; then consider Z being set such that A34:x in Z & Z in rng H by TARSKI:def 4; dom H = NAT by FUNCT_2:def 1; then consider n being set such that A35:n in NAT & Z = H.n by A34,FUNCT_1:def 5; reconsider n as Element of NAT by A35; A36: x in H.n & H.n c= L.n by A20,A34,A35; n in dom L by A35,FUNCT_2:def 1; then L.n in rng L by FUNCT_1:def 5; hence thesis by A36,TARSKI:def 4; end; then A37:C c= union rng L by A27,XBOOLE_1:1; for A being set holds A in rng L implies A is measure_zero of M proof let A be set; assume A38:A in rng L; A39: rng L c= S by MEASURE2:def 1; dom L = NAT by FUNCT_2:def 1; then A40: ex n being set st n in NAT & A = L.n by A38,FUNCT_1:def 5; reconsider A as Element of S by A38,A39; M.A = 0. by A20,A40; hence thesis by MEASURE1:def 13; end; then union rng L is measure_zero of M by MEASURE2:16; then M.(union rng L) = 0. by MEASURE1:def 13; hence thesis by A37,Def3; end; then consider C being thin of M such that A41:union K = B \/ C by A26; take C; thus thesis by A41; end; take B; thus thesis by A25; end; hence thesis by A1; end; hence thesis by A2,MEASURE1:def 3,def 9; end; 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; coherence proof for A being set holds (A in COM(S,M) iff (ex B being set st B in S & ex C being thin of M st A = B \/ C)) by Def4; hence thesis by Th21; end; end; theorem Th22: 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 proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let B1,B2 be set; assume A1:B1 in S & B2 in S; let C1,C2 be thin of M; assume A2:B1 \/ C1 = B2 \/ C2; consider D1 being set such that A3:D1 in S & C1 c= D1 & M.D1 = 0. by Def3; consider D2 being set such that A4:D2 in S & C2 c= D2 & M.D2 = 0. by Def3; B1 c= B2 \/ C2 & B2 \/ C2 c= B2 \/ D2 by A2,A4,XBOOLE_1:7,9 ; then A5:B1 c= B2 \/ D2 by XBOOLE_1:1; B2 c= B1 \/ C1 & B1 \/ C1 c= B1 \/ D1 by A2,A3,XBOOLE_1:7,9 ; then A6:B2 c= B1 \/ D1 by XBOOLE_1:1; reconsider B1,B2,D1,D2 as Element of S by A1,A3,A4; A7:M.B1 <=' M.(B2 \/ D2) by A5,MEASURE1:62; A8:M.(B2 \/ D2) <=' M.B2 + M.D2 by MEASURE1:64; M.B2 + M.D2 = M.B2 by A4,SUPINF_2:18; then A9:M.B1 <=' M.B2 by A7,A8,SUPINF_1:29; A10:M.B2 <=' M.(B1 \/ D1) by A6,MEASURE1:62; A11:M.(B1 \/ D1) <=' M.B1 + M.D1 by MEASURE1:64; M.B1 + M.D1 = M.B1 by A3,SUPINF_2:18; then M.B2 <=' M.B1 by A10,A11,SUPINF_1:29; hence thesis by A9,SUPINF_1:22; end; 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 :Def6:for B being set st B in S for C being thin of M holds it.(B \/ C) = M.B; existence proof defpred P[set,set] means for x,y being set st x in COM(S,M) holds (x =$1 & y = \$2 implies (for B being set st B in S
for C being thin of M holds (x = B \/ C implies y = M.B)));
A1: for x being set st x in COM(S,M)
ex y being set st y in ExtREAL & P[x,y]
proof
let x be set;
assume x in COM(S,M);
then consider B being set such that
A2:B in S & ex C being thin of M st x = B \/ C by Def4;
take M.B;
thus thesis by A2,Th22,FUNCT_2:7;
end;
consider comM being Function of COM(S,M),ExtREAL such that
A3: for x being set st x in COM(S,M) holds P[x,comM.x] from FuncEx1(A1);
A4: comM is nonnegative
proof
for x being Element of COM(S,M) holds 0. <=' comM.x
proof
let x be Element of COM(S,M);
consider B being set such that
A5:B in S & ex C being thin of M st x = B \/ C by Def4;
reconsider B as Element of S by A5;
A6:     comM.x = M.B by A3,A5;
M is nonnegative by MEASURE1:def 11;
hence thesis by A6,MEASURE1:def 4;
end;
hence thesis by MEASURE1:def 4;
end;
A7: for B being set st B in S
for C being thin of M holds comM.(B \/ C) = M.B
proof
let B be set;
assume
A8:B in S;
let C be thin of M;
B \/ C in COM(S,M) by A8,Def4;
hence thesis by A3,A8;
end;
{} is thin of M
proof
A9:ex B1 being set st B1 in S & {} c= B1 & M.B1 = 0.
proof
take {};
thus thesis by MEASURE1:45,def 11;
end;
{} is Subset of X by XBOOLE_1:2;
hence thesis by A9,Def3;
end;
then reconsider C = {} as thin of M;
set B = {};
A10:B in S by MEASURE1:45;
{} = B \/ C;
then A11:comM.{} = M.{} by A7,A10
.= 0. by MEASURE1:def 11;
for F being Sep_Sequence of COM(S,M) holds
SUM(comM*F) = comM.(union rng F)
proof
let F be Sep_Sequence of COM(S,M);
A12:dom F = NAT by FUNCT_2:def 1;
consider G being Function of NAT,S such that
A13:for n being Element of NAT holds G.n in MeasPart(F.n) by Th18;
A14:for n being Element of NAT holds G.n in S & G.n c= F.n &
F.n \ G.n is thin of M
proof
let n be Element of NAT;
G.n in MeasPart(F.n) by A13;
hence thesis by Def5;
end;
consider H be Function of NAT,bool X such that
A15:for n being Element of NAT holds (H.n = F.n \ G.n) by Th19;
for n being Element of NAT holds H.n is thin of M
proof
let n be Element of NAT;
F.n \ G.n is thin of M by A14;
hence thesis by A15;
end;
then consider L being Function of NAT,S such that
A16:for n being Element of NAT holds H.n c= L.n & M.(L.n) = 0. by Th20;
consider B being set such that
A17:B = union rng G;
A18:B c= union rng F
proof
let x be set;
assume x in B;
then consider Z being set such that
A19:x in Z & Z in rng G by A17,TARSKI:def 4;
dom G = NAT by FUNCT_2:def 1;
then consider n being set such that
A20:n in NAT & Z = G.n by A19,FUNCT_1:def 5;
reconsider n as Element of NAT by A20;
set P = F.n;
A21:        G.n c= P by A14;
ex P being set st P in rng F & x in P
proof
take P;
thus thesis by A12,A19,A20,A21,FUNCT_1:def 5;
end;
hence thesis by TARSKI:def 4;
end;
A22:  ex C being thin of M st union rng F = B \/ C
proof
set C = union rng F \ B;
A23:union rng F = C \/ union rng F /\ B by XBOOLE_1:51
.= B \/ C by A18,XBOOLE_1:28;
C c= X
proof
union rng F \ B c= union rng F by XBOOLE_1:36;
hence thesis by XBOOLE_1:1;
end;
then reconsider C as Subset of X;
C is thin of M
proof
A24:C c= union rng H
proof
let x be set;
assume x in C;
then A25:x in union rng F & not x in union rng G by A17,XBOOLE_0:def
4;
then consider Z being set such that
A26:x in Z & Z in rng F by TARSKI:def 4;
consider n being set such that
A27:n in NAT & Z = F.n by A12,A26,FUNCT_1:def 5;
reconsider n as Element of NAT by A27;
not x in G.n
proof
assume
A28:x in G.n;
dom G = NAT by FUNCT_2:def 1;
then G.n in rng G by FUNCT_1:def 5;
hence thesis by A25,A28,TARSKI:def 4;
end;
then A29:           x in F.n \ G.n by A26,A27,XBOOLE_0:def 4;
ex Z being set st x in Z & Z in rng H
proof
A30:              dom H = NAT by FUNCT_2:def 1;
take H.n;
thus thesis by A15,A29,A30,FUNCT_1:def 5;
end;
hence thesis by TARSKI:def 4;
end;
union rng H c= union rng L
proof
let x be set;
assume x in union rng H;
then consider Z being set such that
A31:x in Z & Z in rng H by TARSKI:def 4;
dom H = NAT by FUNCT_2:def 1;
then consider n being set such that
A32:n in NAT & Z = H.n by A31,FUNCT_1:def 5;
reconsider n as Element of NAT by A32;
A33: x in H.n & H.n c= L.n by A16,A31,A32;
n in dom L by A32,FUNCT_2:def 1;
then L.n in rng L by FUNCT_1:def 5;
hence thesis by A33,TARSKI:def 4;
end;
then A34:C c= union rng L by A24,XBOOLE_1:1;
M.(union rng L) = 0.
proof
for A being set holds A in rng L implies
A is measure_zero of M
proof
let A be set;
assume
A35:A in rng L;
A36:              rng L c= S by MEASURE2:def 1;
dom L = NAT by FUNCT_2:def 1;
then A37: ex n being set st
n in NAT & A = L.n by A35,FUNCT_1:def 5;
reconsider A as Element of S by A35,A36;
M.A = 0. by A16,A37;
hence thesis by MEASURE1:def 13;
end;
then union rng L is measure_zero of M by MEASURE2:16;
hence thesis by MEASURE1:def 13;
end;
hence thesis by A34,Def3;
end;
then consider C being thin of M such that
A38:union rng F = B \/ C by A23;
take C;
thus thesis by A38;
end;
for n,m being set st n <> m holds G.n misses G.m
proof
let n,m be set;
assume n <> m;
then F.n misses F.m by PROB_2:def 3;
then A39:F.n /\ F.m = {} by XBOOLE_0:def 7;
A40:       dom F = NAT by FUNCT_2:def 1 .= dom G by FUNCT_2:def 1;
for n being set holds G.n c= F.n
proof
let n be set;
per cases;
suppose n in dom F;
then n in NAT by FUNCT_2:def 1;
hence thesis by A14;
suppose A41:not n in dom F;
then F.n = {} by FUNCT_1:def 4 .= G.n by A40,A41,FUNCT_1:def 4;
hence thesis;
end;
then G.n c= F.n & G.m c= F.m;
then G.n /\ G.m c= {} by A39,XBOOLE_1:27;
then G.n /\ G.m = {} by XBOOLE_1:3;
hence thesis by XBOOLE_0:def 7;
end;
then reconsider G as Sep_Sequence of S by PROB_2:def 3;
A42:SUM(M*G) = M.(union rng G) by MEASURE1:def 11;
A43:comM*F is nonnegative by A4,MEASURE1:54;
M is nonnegative by MEASURE1:def 11;
then A44:M*G is nonnegative by MEASURE1:54;
SUM(comM*F) = SUM(M*G)
proof
A45:for n being Nat holds comM.(F.n) = M.(G.n)
proof
let n be Nat;
A46:G.n in S & G.n c= F.n & F.n \ G.n is thin of M by A14;
then consider C being thin of M such that
A47:C = F.n \ G.n;
F.n = (F.n /\ G.n) \/ (F.n \ G.n) by XBOOLE_1:51
.= G.n \/ C by A46,A47,XBOOLE_1:28;
hence thesis by A7;
end;
A48:for n being Nat holds (comM*F).n = (M*G).n
proof
let n be Nat;
(comM*F).n = comM.(F.n) by FUNCT_2:21
.= M.(G.n) by A45
.= (M*G).n by FUNCT_2:21;
hence thesis;
end;
then for n being Nat holds (comM*F).n <=' (M*G).n;
then A49:SUM(comM*F) <=' SUM(M*G) by A43,SUPINF_2:62;
for n being Nat holds (M*G).n <=' (comM*F).n by A48;
then SUM(M*G) <=' SUM(comM*F) by A44,SUPINF_2:62;
hence thesis by A49,SUPINF_1:22;
end;
hence thesis by A7,A17,A22,A42;
end;
then reconsider comM as sigma_Measure of COM(S,M) by A4,A11,MEASURE1:def 11;
take comM;
thus thesis by A7;
end;
uniqueness
proof
let M1,M2 be sigma_Measure of COM(S,M) such that
A50:(for B being set st B in S
for C being thin of M holds M1.(B \/ C) = M.B) and
A51:(for B being set st B in S
for C being thin of M holds M2.(B \/ C) = M.B);
for x being set holds x in COM(S,M) implies M1.x = M2.x
proof
let x be set;
assume x in COM(S,M);
then consider B being set such that
A52:B in S & ex C being thin of M st x = B \/ C by Def4;
M1.x = M.B by A50,A52
.= M2.x by A51,A52;
hence thesis;
end;
hence thesis by FUNCT_2:18;
end;
end;

theorem
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
COM(M) is_complete COM(S,M)
proof
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
for A being Subset of X for B being set st B in COM(S,M) holds
((A c= B & (COM(M)).B = 0.) implies A in COM(S,M))
proof
let A be Subset of X;
let B be set;
assume
A1:B in COM(S,M);
assume
A2:A c= B & (COM(M)).B = 0.;
ex B1 being set st (B1 in S & ex C1 being thin of M st A = B1 \/ C1)
proof
consider B2 being set such that
A3:B2 in S & ex C2 being thin of M st B = B2 \/ C2 by A1,Def4;
consider C2 being thin of M such that
A4:B = B2 \/ C2 by A3;
A5:M.B2 = 0. by A2,A3,Def6;
consider D2 being set such that
A6:D2 in S & C2 c= D2 & M.D2 = 0. by Def3;
set C1 = (A /\ B2) \/ (A /\ C2);
A7:A = A /\ (B2 \/ C2) by A2,A4,XBOOLE_1:28
.= {} \/ C1 by XBOOLE_1:23;
set O = B2 \/ D2;
A8:O in S by A3,A6,MEASURE1:46;
A /\ B2 c= B2 & A /\ C2 c= C2 by XBOOLE_1:17;
then A9:            A /\ B2 c= B2 & A /\ C2 c= D2 by A6,XBOOLE_1:1;
then A10:C1 c= O by XBOOLE_1:13;
A11:C1 is thin of M
proof
A12:ex O being set st (O in S & C1 c= O & M.O = 0.)
proof
consider O1 being Element of S such that
A13:O1 = O by A8;
reconsider B2,D2 as Element of S by A3,A6;
M.(B2 \/ D2) <=' 0. + 0. by A5,A6,MEASURE1:64;
then A14:M.O1 <=' 0. by A13,SUPINF_2:18;
M is nonnegative by MEASURE1:def 11;
then A15:                  0. <=' M.O1 by MEASURE1:def 4;
take O;
thus thesis by A9,A13,A14,A15,SUPINF_1:22,XBOOLE_1:13;
end;
C1 c= X by A8,A10,XBOOLE_1:1;
hence thesis by A12,Def3;
end;
take {};
thus thesis by A7,A11,MEASURE1:45;
end;
hence thesis by Def4;
end;
hence thesis by Def2;
end;