### The Mizar article:

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

**by****Jozef Bialas**

- Received July 3, 1991
Copyright (c) 1991 Association of Mizar Users

- MML identifier: MEASURE2
- [ MML identifier index ]

environ vocabulary MEASURE1, FUNCT_1, SUPINF_2, BOOLE, SETFAM_1, TARSKI, RELAT_1, ARYTM_3, RLVECT_1, PROB_1, ORDINAL2, MEASURE2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1; constructors NAT_1, SUPINF_2, MEASURE1, PROB_2, MEMBERED, XBOOLE_0; clusters SUBSET_1, SUPINF_1, MEASURE1, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1, ENUMSET1, REAL_1, RELSET_1, PROB_2, XBOOLE_0, XBOOLE_1; schemes NAT_1, RECDEF_1; begin :: :: Some useful theorems about measures and functions :: reserve X for set; theorem Th1: for S being sigma_Field_Subset of X, M being sigma_Measure of S, F being Function of NAT,S holds M*F is nonnegative proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, F be Function of NAT,S; M is nonnegative by MEASURE1:def 11; hence thesis by MEASURE1:54; end; definition let X be set; let S be sigma_Field_Subset of X; mode N_Measure_fam of S -> N_Sub_set_fam of X means :Def1: it c= S; existence proof A1:{} is Subset of X by XBOOLE_1:2; {{},{}} = {{}} by ENUMSET1:69; then A2:{{}} is N_Sub_set_fam of X by A1,MEASURE1:41; A3:{} in S by MEASURE1:45; consider C being N_Sub_set_fam of X such that A4:C = {{}} by A2; take C; thus thesis by A3,A4,ZFMISC_1:37; end; end; canceled; theorem Th3: for S being sigma_Field_Subset of X, T being N_Measure_fam of S holds meet T in S & union T in S proof let S be sigma_Field_Subset of X, T be N_Measure_fam of S; T c= S by Def1; hence thesis by MEASURE1:49,def 9; end; definition let X be set; let S be sigma_Field_Subset of X; let T be N_Measure_fam of S; redefine func meet T -> Element of S; coherence by Th3; redefine func union T -> Element of S; coherence by Th3; end; theorem Th4: for S being sigma_Field_Subset of X, N being Function of NAT,S holds ex F being Function of NAT,S st F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n proof let S be sigma_Field_Subset of X, N be Function of NAT,S; reconsider S as non empty set; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds c = $1 & A = $2 & B = $3 implies B = N.(c+1) \ N.(c); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; reconsider B = N.(c+1) \ N.c as Element of S; take B; thus thesis; end; reconsider A = N.0 as Element of S; consider F being Function of NAT,S such that A2:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)]) from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.(n+1) \ N.n proof let n be Element of NAT; for a,b being Element of S,s being Nat st s = n & a = F.n & b = F.(n+1) holds b = N.(s+1) \ N.s by A2; hence thesis; end; hence thesis by A2; end; theorem Th5: for S being sigma_Field_Subset of X, N being Function of NAT,S holds ex F being Function of NAT,S st F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n proof let S be sigma_Field_Subset of X, N be Function of NAT,S; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds (c = $1 & A = $2 & B = $3 implies B = (N.(c+1)) \/ A); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; reconsider B = N.(c+1) \/ A as Element of S; take B; thus thesis; end; consider F being Function of NAT,S such that A2:F.0 = (N.0) & for n being Element of NAT holds P[n,F.n,F.(n+1)] from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.(n+1) \/ F.n by A2; hence thesis by A2; end; theorem Th6: for S being non empty Subset-Family of X, N,F being Function of NAT,S holds F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n) implies (for r being set for n being Nat holds (r in F.n iff ex k being Nat st (k <= n & r in N.k))) proof let S be non empty Subset-Family of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n); let r be set; let n be Nat; thus r in F.n implies ex k being Nat st k <= n & r in N.k proof defpred P[Nat] means r in F.$1; assume A2:r in F.n; then A3:ex n being Nat st P[n]; ex s being Nat st P[s] & for k being Nat st P[k] holds s <= k from Min(A3); then consider s being Nat such that A4:r in F.s & for k being Nat st r in F.k holds s <= k; A5:s=0 implies ex k being Nat st k <= n & r in N.k proof assume A6: s = 0; take 0; thus thesis by A1,A4,A6,NAT_1:18; end; (ex k being Nat st s = k + 1) implies (ex k being Nat st k <= n & r in N.k) proof given k being Nat such that A7:s = k + 1; A8: F.s = N.s \/ F.k by A1,A7; A9: not r in F.k proof assume r in F.k; then s <= k by A4; hence thesis by A7,NAT_1:38; end; take s; thus thesis by A2,A4,A8,A9,XBOOLE_0:def 2; end; hence thesis by A5,NAT_1:22; end; defpred P[Nat] means (ex k being Nat st k <= $1 & r in N.k) implies r in F.$1; A10: P[0] by A1,NAT_1:19; A11:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A12:(ex k being Nat st k <= n & r in N.k) implies r in F.n; given k being Nat such that A13:k <= n+1 & r in N.k; A14:F.(n+1) = N.(n+1) \/ F.n by A1; k <= n or k = n + 1 by A13,NAT_1:26; hence thesis by A12,A13,A14,XBOOLE_0:def 2; end; for n being Nat holds P[n] from Ind(A10,A11); hence thesis; end; theorem Th7: for S being non empty Subset-Family of X, N,F being Function of NAT,S holds (F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n) implies for n,m being Nat st n < m holds F.n c= F.m) proof let S be non empty Subset-Family of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n; defpred X[Nat] means for m being Nat st $1 < m holds F.$1 c= F.m; A2: X[0] proof let m be Nat; assume A3:0 < m; A4:for k being Nat st 0 < k + 1 holds F.0 c= F.(k+1) proof defpred P[Nat] means 0 < $1 + 1 implies F.0 c= F.($1+1); F.(0+1) = N.(0+1) \/ F.0 by A1; then A5: P[0] by XBOOLE_1:7; A6:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A7:0 < k + 1 implies F.0 c= F.(k+1); F.(k+1+1) = N.(k+1+1) \/ F.(k+1) by A1; then A8:F.(k+1) c= F.(k+1+1) by XBOOLE_1:7; 0 <= k by NAT_1:18; hence thesis by A7,A8,NAT_1:38,XBOOLE_1:1; end; thus for k being Nat holds P[k] from Ind(A5,A6); end; ex k being Nat st m = k + 1 by A3,NAT_1:22; hence thesis by A3,A4; end; A9:for n being Nat st X[n] holds X[n+1] proof let n be Nat; assume A10:for m being Nat st n < m holds F.n c= F.m; let m be Nat; assume A11:n+1 < m; let r be set; assume A12:r in F.(n+1); A13: F.(n+1) = N.(n+1) \/ F.n by A1; A14:r in N.(n+1) implies r in F.m by A1,A11,Th6; r in F.n implies r in F.m proof assume A15:r in F.n; n < m implies r in F.m proof assume n < m; then F.n c= F.m by A10; hence thesis by A15; end; hence thesis by A11,NAT_1:38; end; hence thesis by A12,A13,A14,XBOOLE_0:def 2; end; thus for n being Nat holds X[n] from Ind(A2,A9); end; theorem Th8: for S being non empty Subset-Family of X, N, G, F being Function of NAT,S holds (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n)) implies (for n,m being Nat st n <= m holds F.n c= G.m) proof let S be non empty Subset-Family of X, N, G, F be Function of NAT,S; assume A1:(G.0 = N.0) & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & (F.0 = N.0) & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n); A2:for n being Nat holds F.n c= G.n proof defpred P[Nat] means F.$1 c= G.$1; A3: P[0] by A1; A4:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume F.n c= G.n; F.(n+1) = N.(n+1) \ G.n by A1; then A5:F.(n+1) c= N.(n+1) by XBOOLE_1:36; G.(n+1) = N.(n+1) \/ G.n by A1; then N.(n+1) c= G.(n+1) by XBOOLE_1:7; hence thesis by A5,XBOOLE_1:1; end; thus for n being Nat holds P[n] from Ind(A3,A4); end; let n,m be Nat; assume n <= m; then A6:n = m or n < m by REAL_1:def 5; n < m implies F.n c= G.m proof assume A7:n < m; A8:F.n c= G.n by A2; G.n c= G.m by A1,A7,Th7; hence thesis by A8,XBOOLE_1:1; end; hence thesis by A2,A6; end; theorem Th9: for S being sigma_Field_Subset of X holds for N, G being Function of NAT,S holds ex F being Function of NAT,S st F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n proof let S be sigma_Field_Subset of X; let N, G be Function of NAT,S; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds (c = $1 & A = $2 & B = $3 implies B = (N.(c+1)) \ G.c); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; consider B being set such that A2:B = N.(c+1) \ G.c; reconsider B as Element of S by A2; take B; thus thesis by A2; end; consider F being Function of NAT,S such that A3:F.0 = N.0 & for n being Element of NAT holds P[n,F.n,F.(n+1)] from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.(n+1) \ G.n proof let n be Element of NAT; for a,b being Element of S,s being Nat st s = n & a = F.n & b = F.(n+1) holds b = N.(s+1) \ G.s by A3; hence thesis; end; hence thesis by A3; end; theorem for S being sigma_Field_Subset of X holds for N being Function of NAT,S holds ex F being Function of NAT,S st F.0 = {} & for n being Element of NAT holds F.(n+1) = N.0 \ N.n proof let S be sigma_Field_Subset of X; let N be Function of NAT,S; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds (c = $1 & A = $2 & B = $3 implies B = N.0 \ N.(c)); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; reconsider B = N.0 \ N.c as Element of S; take B; thus thesis; end; reconsider A = {} as Element of S by MEASURE1:45; consider F being Function of NAT,S such that A2:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)]) from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.0 \ N.n proof let n be Element of NAT; for a,b being Element of S,s being Nat st s = n & a = F.n & b = F.(n+1) holds b = N.0 \ N.s by A2; hence thesis; end; hence thesis by A2; end; theorem Th11: for S being sigma_Field_Subset of X holds for N, G, F being Function of NAT,S holds (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n)) implies (for n,m being Nat st n < m holds F.n misses F.m) proof let S be sigma_Field_Subset of X; let N, G, F be Function of NAT,S; assume A1:G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n); let n,m be Nat; assume A2:n < m; then 0 <= m & 0 <> m by NAT_1:18; then consider k being Nat such that A3:m = k + 1 by NAT_1:22; F.(k+1) = N.(k+1) \ G.k by A1; then A4:G.k misses F.(k+1) by XBOOLE_1:79; n <= k by A2,A3,NAT_1:38; then F.n c= G.k by A1,Th8; hence F.n /\ F.m = (F.n /\ G.k) /\ F.(k+1) by A3,XBOOLE_1:28 .= F.n /\ (G.k /\ F.(k+1)) by XBOOLE_1:16 .= F.n /\ {} by A4,XBOOLE_0:def 7 .= {}; end; canceled; theorem Th13: for S being sigma_Field_Subset of X, M being sigma_Measure of S, T being N_Measure_fam of S, F being Function of NAT,S st T = rng F holds M.(union T) <=' SUM(M*F) proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, T be N_Measure_fam of S, F be Function of NAT,S; assume A1:T = rng F; consider G being Function of NAT,S such that A2:G.0 = F.0 & for n being Element of NAT holds G.(n+1) = F.(n+1) \/ G.n by Th5; consider H being Function of NAT,S such that A3:H.0 = F.0 & for n being Element of NAT holds H.(n+1) = F.(n+1) \ G.n by Th9; A4:for n being Element of NAT holds H.n c= F.n proof let n be Element of NAT; A5:n=0 or ex k being Nat st n = k + 1 by NAT_1:22; (ex k being Nat st n = k + 1) implies H.n c= F.n proof given k being Nat such that A6:n = k + 1; H.n = F.n \ G.k by A3,A6; hence thesis by XBOOLE_1:36; end; hence thesis by A3,A5; end; A7:for n being Element of NAT holds (M*H).n <=' (M*F).n proof let n be Element of NAT; NAT = dom(M*H) & NAT = dom(M*F) by FUNCT_2:def 1; then A8:(M*H).n = M.(H.n) & (M*F).n = M.(F.n) by FUNCT_1:22; consider A,B being Element of S such that A9:A = H.n & B = F.n; A c= B by A4,A9; hence thesis by A8,A9,MEASURE1:62; end; A10: M*H is nonnegative by Th1; for n,m being set st n <> m holds H.n misses H.m proof let n,m be set; assume A11: n <> m; per cases; suppose n in dom H & m in dom H; then reconsider n'=n,m'=m as Nat by FUNCT_2:def 1; A12:n' < m' implies H.n misses H.m by A2,A3,Th11; m' < n' implies H.m misses H.n by A2,A3,Th11; hence H.n misses H.m by A11,A12,REAL_1:def 5; suppose not (n in dom H & m in dom H); then H.n = {} or H.m = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; then H is Sep_Sequence of S by PROB_2:def 3; then A13:SUM(M*H) = M.(union rng H) by MEASURE1:def 11; union rng H = union rng F proof thus union rng H c= union rng F proof let r be set; assume r in union rng H; then consider E being set such that A14:r in E & E in rng H by TARSKI:def 4; consider s being set such that A15:s in dom H & E = H.s by A14,FUNCT_1:def 5; reconsider s as Element of NAT by A15,FUNCT_2:def 1; A16: E c= F.s by A4,A15; F.s in rng F by FUNCT_2:6; hence thesis by A14,A16,TARSKI:def 4; end; let r be set; assume r in union rng F; then consider E being set such that A17:r in E & E in rng F by TARSKI:def 4; consider s being set such that A18:s in dom F & E = F.s by A17,FUNCT_1:def 5; reconsider s as Element of NAT by A18,FUNCT_2:def 1; ex s1 being Element of NAT st r in H.s1 proof defpred P[Nat] means r in F.$1; r in F.s by A17,A18; then A19:ex k being Nat st P[k]; ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from Min(A19); then consider k being Nat such that A20:r in F.k & for n being Nat st r in F.n holds k <= n; A21:k=0 implies ex s1 being Element of NAT st r in H.s1 by A3,A20; (ex l being Nat st k = l + 1) implies (ex s1 being Element of NAT st r in H.s1) proof given l being Nat such that A22:k = l + 1; A23:not r in G.l proof assume r in G.l; then consider i being Nat such that A24:i <= l & r in F.i by A2,Th6; k <= i by A20,A24; hence thesis by A22,A24,NAT_1:38; end; A25: H.(l+1) = F.(l+1) \ G.l by A3; take k; thus thesis by A20,A22,A23,A25,XBOOLE_0:def 4; end; hence thesis by A21,NAT_1:22; end; then consider s1 being Element of NAT such that A26:r in H.s1; H.s1 in rng H by FUNCT_2:6; hence thesis by A26,TARSKI:def 4; end; hence thesis by A1,A7,A10,A13,SUPINF_2:62; end; theorem Th14: for S being sigma_Field_Subset of X, T being N_Measure_fam of S holds ex F being Function of NAT,S st T = rng F proof let S be sigma_Field_Subset of X, T be N_Measure_fam of S; consider F being Function of NAT,bool X such that A1:T = rng F by SUPINF_2:def 14; rng F c= S by A1,Def1; then F is Function of NAT,S by FUNCT_2:8; then consider F being Function of NAT,S such that A2:T = rng F by A1; take F; thus thesis by A2; end; theorem Th15: for S being sigma_Field_Subset of X, N, F being Function of NAT,S st (F.0 = {} & for n being Element of NAT holds (F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n)) holds for n being Element of NAT holds F.n c= F.(n+1) proof let S be sigma_Field_Subset of X; let N,F be Function of NAT,S; assume A1:F.0 = {} & for n being Element of NAT holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n; let n be Element of NAT; defpred P[Nat] means F.$1 c= F.($1+1); F.(0+1) = N.0 \ N.0 by A1; then A2: P[0] by A1,XBOOLE_1:37; A3:for n be Nat st P[n] holds P[n+1] proof let n be Nat; assume F.n c= F.(n+1); A4:F.((n+1)+1) = N.0 \ N.(n+1) by A1; N.(n+1) c= N.n by A1; then N.0 \ N.n c= F.((n+1)+1) by A4,XBOOLE_1:34; hence thesis by A1; end; for n being Element of NAT holds P[n] from Ind(A2,A3); hence thesis; end; theorem for S being sigma_Field_Subset of X, M being sigma_Measure of S, T being N_Measure_fam of S holds (for A being set holds A in T implies A is measure_zero of M) implies union T is measure_zero of M proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, T be N_Measure_fam of S; assume A1:for A being set holds A in T implies A is measure_zero of M; consider F being Function of NAT,S such that A2:T = rng F by Th14; set G = M*F; A3:G is nonnegative by Th1; A4:for r being Nat holds 0 <= r implies G.r = 0. proof let r be Nat; F.r in T & F.r is Element of S by A2,FUNCT_2:6; then F.r is measure_zero of M by A1; then M.(F.r) = 0. by MEASURE1:def 13; hence thesis by FUNCT_2:21; end; then SUM(G) = Ser(G).0 by A3,SUPINF_2:67; then SUM(G) = G.0 by SUPINF_2:63; then SUM(M*F) = 0. by A4; then A5:M.(union T) <=' 0. by A2,Th13; M is nonnegative by MEASURE1:def 11; then 0. <=' M.(union T) by MEASURE1:def 4; then M.(union T) = 0. by A5,SUPINF_1:22; hence thesis by MEASURE1:def 13; end; theorem Th17: for S being sigma_Field_Subset of X, M being sigma_Measure of S, T being N_Measure_fam of S st (ex A being set st A in T & A is measure_zero of M) holds meet T is measure_zero of M proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, T be N_Measure_fam of S; given A being set such that A1: A in T & A is measure_zero of M; meet T c= A by A1,SETFAM_1:4; hence thesis by A1,MEASURE1:69; end; theorem for S being sigma_Field_Subset of X, M being sigma_Measure of S, T being N_Measure_fam of S st (for A being set holds A in T implies A is measure_zero of M) holds meet T is measure_zero of M proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, T be N_Measure_fam of S; assume A1:for A being set holds A in T implies A is measure_zero of M; ex A being set st A in T & A is measure_zero of M proof consider F being Function of NAT,bool X such that A2: T = rng F by SUPINF_2:def 14; A3: F.0 in T by A2,FUNCT_2:6; take F.0; thus thesis by A1,A3; end; hence thesis by Th17; end; definition let X be set; let S be sigma_Field_Subset of X; let IT be N_Measure_fam of S; attr IT is non-decreasing means :Def2:ex F being Function of NAT,S st IT = rng F & for n being Element of NAT holds F.n c= F.(n+1); end; definition let X be set; let S be sigma_Field_Subset of X; cluster non-decreasing N_Measure_fam of S; existence proof {} in S by MEASURE1:45; then consider A being set such that A1:A in S; reconsider A as Subset of X by A1; consider B,C being Subset of X such that A2:B = A & C = A; consider F being Function of NAT,bool X such that A3:rng F = {B,C} & F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:40; A4:rng F = {A} & F.0 = A & for n being Nat st 0 < n holds F.n = A by A2,A3,ENUMSET1:69; then rng F c= S by A1,ZFMISC_1:37; then reconsider F as Function of NAT,S by FUNCT_2:8; A5:{A} is N_Sub_set_fam of X by A4,MEASURE1:6,SUPINF_2:def 14; {A} c= S by A1,ZFMISC_1:37; then reconsider T = {A} as N_Measure_fam of S by A5,Def1; take T,F; for n being Element of NAT holds F.n c= F.(n+1) proof let n be Element of NAT; for n being Nat holds F.n = A proof let n be Nat; n = 0 or 0 < n by NAT_1:19; hence thesis by A2,A3; end; then F.n = A & F.(n + 1) = A; hence thesis; end; hence thesis by A2,A3,ENUMSET1:69; end; end; definition let X be set; let S be sigma_Field_Subset of X; let IT be N_Measure_fam of S; attr IT is non-increasing means ex F being Function of NAT,S st (IT = rng F & for n being Element of NAT holds F.(n+1) c= F.n); end; definition let X be set; let S be sigma_Field_Subset of X; cluster non-increasing N_Measure_fam of S; existence proof {} in S by MEASURE1:45; then consider A being set such that A1:A in S; reconsider A as Subset of X by A1; set B = A, C = A; consider F being Function of NAT,bool X such that A2:rng F = {B,C} & F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:40; A3:rng F = {A} & F.0 = A & for n being Nat st 0 < n holds F.n = A by A2,ENUMSET1:69; then rng F c= S by A1,ZFMISC_1:37; then reconsider F as Function of NAT,S by FUNCT_2:8; A4:{A} is N_Sub_set_fam of X by A3,MEASURE1:6,SUPINF_2:def 14; {A} c= S by A1,ZFMISC_1:37; then reconsider T = {A} as N_Measure_fam of S by A4,Def1; take T,F; for n being Element of NAT holds F.(n+1) c= F.n proof let n be Element of NAT; for n being Nat holds F.n = A proof let n be Nat; n = 0 or 0 < n by NAT_1:19; hence thesis by A2; end; then F.n = A & F.(n + 1) = A; hence thesis; end; hence thesis by A2,ENUMSET1:69; end; end; canceled 2; theorem for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = {} & for n being Element of NAT holds (F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n)) implies rng F is non-decreasing N_Measure_fam of S proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume F.0 = {} & for n being Element of NAT holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n; then A1:for n being Element of NAT holds F.n c= F.(n+1) by Th15; A2:rng F c= S by RELSET_1:12; rng F is N_Sub_set_fam of X by MEASURE1:52; hence thesis by A1,A2,Def1,Def2; end; theorem Th22: for S being non empty Subset-Family of X, N being Function of NAT,S holds (for n being Element of NAT holds N.n c= N.(n+1)) implies (for m,n being Nat st n < m holds N.n c= N.m) proof let S be non empty Subset-Family of X, N be Function of NAT,S; assume A1:for n being Element of NAT holds N.n c= N.(n+1); defpred P[Nat] means for n being Nat st n < $1 holds N.n c= N.$1; A2: P[0] by NAT_1:18; A3:for m being Nat st P[m] holds P[m+1] proof let m be Nat; assume A4:for n being Nat st n < m holds N.n c= N.m; let n be Nat; assume A5:n < m+1; A6:n = m or n < m proof assume A7:n <> m & not n < m; n <= m by A5,NAT_1:38; hence thesis by A7,REAL_1:def 5; end; n < m implies N.n c= N.(m+1) proof assume n < m; then A8:N.n c= N.m by A4; N.m c= N.(m+1) by A1; hence thesis by A8,XBOOLE_1:1; end; hence thesis by A1,A6; end; thus for m being Nat holds P[m] from Ind(A2,A3); end; theorem Th23: for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies (for n,m being Nat st n < m holds F.n misses F.m) proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)); let n,m be Nat; assume A2:n < m; then 0 <= m & 0 <> m by NAT_1:18; then consider k being Nat such that A3:m = k + 1 by NAT_1:22; F.(k+1) = N.(k+1) \ N.k by A1; then A4:N.k misses F.(k+1) by XBOOLE_1:79; A5:n <= k by A2,A3,NAT_1:38; F.n c= N.k proof A6:for n being Nat holds F.n c= N.n proof defpred P[Nat] means F.$1 c= N.$1; A7: P[0] by A1; A8:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume F.n c= N.n; F.(n+1) = N.(n+1) \ N.n by A1; hence thesis by XBOOLE_1:36; end; thus for n being Nat holds P[n] from Ind(A7,A8); end; for n,m being Nat st n <= m holds F.n c= N.m proof let n,m be Nat; assume n <= m; then A9:n = m or n < m by REAL_1:def 5; n < m implies F.n c= N.m proof assume A10:n < m; A11:F.n c= N.n by A6; N.n c= N.m by A1,A10,Th22; hence thesis by A11,XBOOLE_1:1; end; hence thesis by A6,A9; end; hence thesis by A5; end; then F.n /\ F.(k+1) = (F.n /\ N.k) /\ F.(k+1) by XBOOLE_1:28 .= F.n /\ (N.k /\ F.(k+1)) by XBOOLE_1:16 .= F.n /\ {} by A4,XBOOLE_0:def 7 .= {}; hence thesis by A3,XBOOLE_0:def 7; end; theorem Th24: for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies union rng F = union rng N proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1); thus union rng F c= union rng N proof let x be set; assume x in union rng F; then consider Y being set such that A2:x in Y & Y in rng F by TARSKI:def 4; consider n being set such that A3:n in dom F & Y = F.n by A2,FUNCT_1:def 5; reconsider n as Nat by A3,FUNCT_2:def 1; A4:n=0 implies ex Z being set st x in Z & Z in rng N proof assume A5: n=0; take N.0; thus thesis by A1,A2,A3,A5,FUNCT_2:6; end; ex Z being set st x in Z & Z in rng N proof (ex k being Nat st n = k + 1) implies (ex Z being set st x in Z & Z in rng N) proof given k being Nat such that A6:n = k + 1; Y=N.(k+1) \ N.k by A1,A3,A6; then A7:x in N.(k+1) by A2,XBOOLE_0:def 4; consider Z being set such that A8:Z = N.(k+1); Z in rng N by A8,FUNCT_2:6; hence thesis by A7,A8; end; hence thesis by A4,NAT_1:22; end; hence thesis by TARSKI:def 4; end; let x be set; assume x in union rng N; then consider Y being set such that A9:x in Y & Y in rng N by TARSKI:def 4; consider n being set such that A10:n in dom N & Y = N.n by A9,FUNCT_1:def 5; reconsider n as Nat by A10,FUNCT_2:def 1; ex Z being set st x in Z & Z in rng F proof ex s being Element of NAT st x in F.s proof defpred P[Nat] means x in N.$1; x in N.n by A9,A10; then A11:ex k being Nat st P[k]; ex k being Nat st P[k] & for r being Nat st P[r] holds k <= r from Min(A11); then consider k being Nat such that A12:x in N.k & for r being Nat st x in N.r holds k <= r; A13:k=0 implies (ex s being Element of NAT st x in F.s) by A1,A12; (ex l being Nat st k = l + 1) implies (ex s being Element of NAT st x in F.s) proof given l being Nat such that A14:k = l + 1; A15:not x in N.l proof assume x in N.l; then l + 1 <= l by A12,A14; hence thesis by NAT_1:38; end; A16: F.(l+1) = N.(l+1) \ N.l by A1; take k; thus thesis by A12,A14,A15,A16,XBOOLE_0:def 4; end; hence thesis by A13,NAT_1:22; end; then consider s being Element of NAT such that A17:x in F.s; F.s in rng F by FUNCT_2:6; hence thesis by A17; end; hence thesis by TARSKI:def 4; end; theorem Th25: for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies F is Sep_Sequence of S proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1); for n,m being set st n <> m holds F.n misses F.m proof let n,m be set; assume A2: n <> m; per cases; suppose n in dom F & m in dom F; then reconsider n'=n,m'=m as Nat by FUNCT_2:def 1; A3:n' < m' implies F.n misses F.m by A1,Th23; m' < n' implies F.m misses F.n by A1,Th23; hence F.n misses F.m by A2,A3,REAL_1:def 5; suppose not (n in dom F & m in dom F); then F.n = {} or F.m = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; hence thesis by PROB_2:def 3; end; theorem for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies (N.0 = F.0 & for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N.n) proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1); for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N.n proof let n be Element of NAT; F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1) by A1; hence thesis by XBOOLE_1:45; end; hence thesis by A1; end; theorem for S being sigma_Field_Subset of X, M being sigma_Measure of S, F being Function of NAT,S st (for n being Element of NAT holds F.n c= F.(n+1)) holds M.(union rng F) = sup(rng (M*F)) 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 c= F.(n+1); consider G being Function of NAT,S such that A2:G.0 = F.0 & for n being Element of NAT holds G.(n+1) = F.(n+1) \ F.n by Th4; A3:G is Sep_Sequence of S by A1,A2,Th25; A4:rng Ser(M*G) = rng (M*F) proof A5:dom Ser(M*G) = NAT & dom (M*F) = NAT by FUNCT_2:def 1; for m being set st m in NAT holds Ser(M*G).m = (M*F).m proof let m be set; assume A6:m in NAT; defpred P[Nat] means Ser(M*G).$1 = (M*F).$1; A7: P[0] proof thus Ser(M*G).0 = (M*G).0 by SUPINF_2:63 .= M.(F.0) by A2,FUNCT_2:21 .= (M*F).0 by FUNCT_2:21; end; A8:for m being Nat holds P[m] implies P[m+1] proof let m be Nat; assume A9:Ser(M*G).m = (M*F).m; A10:(M*G).(m+1) = M.(G.(m+1)) & (M*F).(m+1) = M.(F.(m+1)) by FUNCT_2:21; A11:G.(m+1) = F.(m+1) \ F.m & F.m c= F.(m+1) by A1,A2; then A12:F.m misses G.(m+1) by XBOOLE_1:79; Ser(M*G).(m + 1) = (M*F).m + (M*G).(m+1) by A9,SUPINF_2:63 .= M.(F.m) + M.(G.(m+1)) by A10,FUNCT_2:21 .= M.(F.m \/ G.(m+1)) by A12,MEASURE1:61 .= (M*F).(m+1) by A10,A11,XBOOLE_1:45; hence thesis; end; for m being Nat holds P[m] from Ind(A7,A8); hence thesis by A6; end; hence thesis by A5,FUNCT_1:9; end; M.(union rng F) = M.(union rng G) by A1,A2,Th24 .= SUM(M*G) by A3,MEASURE1:def 11 .= sup(rng (M*F)) by A4,SUPINF_2:def 23; hence thesis; end;

Back to top