### The Mizar article:

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

**by****Jozef Bialas**

- Received February 22, 1992
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 :: :: Some additional properties about R_eal numbers :: 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; :: :: 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; 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;

Back to top