:: MEASURE2 semantic presentation begin theorem :: MEASURE2:1 for X being set for S being SigmaField of X for M being sigma_Measure of S for F being Function of NAT,S holds M * F is V86() by MEASURE1:25; definition let X be set ; let S be SigmaField of X; mode N_Measure_fam of S -> N_Sub_set_fam of X means :Def1: :: MEASURE2:def 1 it c= S; existence ex b1 being N_Sub_set_fam of X st b1 c= S proof ( {} is Subset of X & {{},{}} = {{}} ) by ENUMSET1:29, XBOOLE_1:2; then reconsider C = {{}} as N_Sub_set_fam of X by MEASURE1:20; take C ; ::_thesis: C c= S {} in S by PROB_1:4; hence C c= S by ZFMISC_1:31; ::_thesis: verum end; end; :: deftheorem Def1 defines N_Measure_fam MEASURE2:def_1_:_ for X being set for S being SigmaField of X for b3 being N_Sub_set_fam of X holds ( b3 is N_Measure_fam of S iff b3 c= S ); theorem Th2: :: MEASURE2:2 for X being set for S being SigmaField of X for T being N_Measure_fam of S holds ( meet T in S & union T in S ) proof let X be set ; ::_thesis: for S being SigmaField of X for T being N_Measure_fam of S holds ( meet T in S & union T in S ) let S be SigmaField of X; ::_thesis: for T being N_Measure_fam of S holds ( meet T in S & union T in S ) let T be N_Measure_fam of S; ::_thesis: ( meet T in S & union T in S ) T c= S by Def1; hence ( meet T in S & union T in S ) by MEASURE1:22, MEASURE1:def_5; ::_thesis: verum end; definition let X be set ; let S be SigmaField of X; let T be N_Measure_fam of S; :: original: meet redefine func meet T -> Element of S; coherence meet T is Element of S by Th2; :: original: union redefine func union T -> Element of S; coherence union T is Element of S by Th2; end; theorem Th3: :: MEASURE2:3 for X being set for S being SigmaField of X for N being Function of NAT,S 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 X be set ; ::_thesis: for S being SigmaField of X for N being Function of NAT,S 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) ) ) let S be SigmaField of X; ::_thesis: for N being Function of NAT,S 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) ) ) let N be Function of NAT,S; ::_thesis: 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) ) ) reconsider S = S as non empty set ; defpred S1[ set , set , set ] means for A, B being Element of S for c being Element of NAT st c = \$1 & A = \$2 & B = \$3 holds B = (N . (c + 1)) \ (N . c); reconsider A = N . 0 as Element of S ; A1: for c being Element of NAT for A being Element of S ex B being Element of S st S1[c,A,B] proof let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B] let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B] reconsider B = (N . (c + 1)) \ (N . c) as Element of S ; take B ; ::_thesis: S1[c,A,B] thus S1[c,A,B] ; ::_thesis: verum end; consider F being Function of NAT,S such that A2: ( F . 0 = A & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) proof let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . (n + 1)) \ (N . n) for a, b being Element of S for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds b = (N . (s + 1)) \ (N . s) by A2; hence F . (n + 1) = (N . (n + 1)) \ (N . n) ; ::_thesis: verum end; hence 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) ) ) by A2; ::_thesis: verum end; theorem Th4: :: MEASURE2:4 for X being set for S being SigmaField of X for N being Function of NAT,S 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 X be set ; ::_thesis: for S being SigmaField of X for N being Function of NAT,S 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) ) ) let S be SigmaField of X; ::_thesis: for N being Function of NAT,S 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) ) ) let N be Function of NAT,S; ::_thesis: 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) ) ) defpred S1[ set , set , set ] means for A, B being Element of S for c being Element of NAT st c = \$1 & A = \$2 & B = \$3 holds B = (N . (c + 1)) \/ A; A1: for c being Element of NAT for A being Element of S ex B being Element of S st S1[c,A,B] proof let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B] let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B] reconsider B = (N . (c + 1)) \/ A as Element of S ; take B ; ::_thesis: S1[c,A,B] thus S1[c,A,B] ; ::_thesis: verum end; consider F being Function of NAT,S such that A2: ( F . 0 = N . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2; hence 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) ) ) by A2; ::_thesis: verum end; theorem Th5: :: MEASURE2:5 for X being set for S being non empty Subset-Family of X for N, 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) ) holds for r being set for n being Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) proof let X be set ; ::_thesis: for S being non empty Subset-Family of X for N, 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) ) holds for r being set for n being Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) let S be non empty Subset-Family of X; ::_thesis: for N, 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) ) holds for r being set for n being Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) let N, F be Function of NAT,S; ::_thesis: ( 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 Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) ) assume that A1: F . 0 = N . 0 and A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; ::_thesis: for r being set for n being Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) let r be set ; ::_thesis: for n being Element of NAT holds ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) let n be Element of NAT ; ::_thesis: ( r in F . n iff ex k being Element of NAT st ( k <= n & r in N . k ) ) defpred S1[ Element of NAT ] means ( ex k being Element of NAT st ( k <= \$1 & r in N . k ) implies r in F . \$1 ); A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: ( ex k being Element of NAT st ( k <= n & r in N . k ) implies r in F . n ) ; ::_thesis: S1[n + 1] A5: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2; given k being Element of NAT such that A6: k <= n + 1 and A7: r in N . k ; ::_thesis: r in F . (n + 1) ( k <= n or k = n + 1 ) by A6, NAT_1:8; hence r in F . (n + 1) by A4, A7, A5, XBOOLE_0:def_3; ::_thesis: verum end; thus ( r in F . n implies ex k being Element of NAT st ( k <= n & r in N . k ) ) ::_thesis: ( ex k being Element of NAT st ( k <= n & r in N . k ) implies r in F . n ) proof defpred S2[ Nat] means r in F . \$1; assume A8: r in F . n ; ::_thesis: ex k being Element of NAT st ( k <= n & r in N . k ) then A9: ex n being Nat st S2[n] ; ex s being Nat st ( S2[s] & ( for k being Nat st S2[k] holds s <= k ) ) from NAT_1:sch_5(A9); then consider s being Nat such that A10: r in F . s and A11: for k being Nat st r in F . k holds s <= k ; A12: ( ex k being Nat st s = k + 1 implies ex k being Element of NAT st ( k <= n & r in N . k ) ) proof given k being Nat such that A13: s = k + 1 ; ::_thesis: ex k being Element of NAT st ( k <= n & r in N . k ) reconsider k = k as Element of NAT by ORDINAL1:def_12; A14: not r in F . k proof assume r in F . k ; ::_thesis: contradiction then s <= k by A11; hence contradiction by A13, NAT_1:13; ::_thesis: verum end; take s ; ::_thesis: ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s ) A15: s in NAT by ORDINAL1:def_12; F . s = (N . s) \/ (F . k) by A2, A13; hence ( s is Element of REAL & s is Element of NAT & s <= n & r in N . s ) by A8, A10, A11, A14, A15, XBOOLE_0:def_3; ::_thesis: verum end; ( s = 0 implies ex k being Element of NAT st ( k <= n & r in N . k ) ) by A1, A10, NAT_1:2; hence ex k being Element of NAT st ( k <= n & r in N . k ) by A12, NAT_1:6; ::_thesis: verum end; A16: S1[ 0 ] by A1, NAT_1:3; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A3); hence ( ex k being Element of NAT st ( k <= n & r in N . k ) implies r in F . n ) ; ::_thesis: verum end; theorem Th6: :: MEASURE2:6 for X being set for S being non empty Subset-Family of X for N, 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) ) holds for n, m being Element of NAT st n < m holds F . n c= F . m proof let X be set ; ::_thesis: for S being non empty Subset-Family of X for N, 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) ) holds for n, m being Element of NAT st n < m holds F . n c= F . m let S be non empty Subset-Family of X; ::_thesis: for N, 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) ) holds for n, m being Element of NAT st n < m holds F . n c= F . m let N, F be Function of NAT,S; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) implies for n, m being Element of NAT st n < m holds F . n c= F . m ) assume that A1: F . 0 = N . 0 and A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ; ::_thesis: for n, m being Element of NAT st n < m holds F . n c= F . m defpred S1[ Element of NAT ] means for m being Element of NAT st \$1 < m holds F . \$1 c= F . m; A3: S1[ 0 ] proof A4: for k being Element of NAT st 0 < k + 1 holds F . 0 c= F . (k + 1) proof defpred S2[ Element of NAT ] means ( 0 < \$1 + 1 implies F . 0 c= F . (\$1 + 1) ); A5: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) A6: 0 <= k by NAT_1:2; F . ((k + 1) + 1) = (N . ((k + 1) + 1)) \/ (F . (k + 1)) by A2; then A7: F . (k + 1) c= F . ((k + 1) + 1) by XBOOLE_1:7; assume ( 0 < k + 1 implies F . 0 c= F . (k + 1) ) ; ::_thesis: S2[k + 1] hence S2[k + 1] by A7, A6, NAT_1:13, XBOOLE_1:1; ::_thesis: verum end; F . (0 + 1) = (N . (0 + 1)) \/ (F . 0) by A2; then A8: S2[ 0 ] by XBOOLE_1:7; thus for k being Element of NAT holds S2[k] from NAT_1:sch_1(A8, A5); ::_thesis: verum end; let m be Element of NAT ; ::_thesis: ( 0 < m implies F . 0 c= F . m ) assume A9: 0 < m ; ::_thesis: F . 0 c= F . m then consider k being Nat such that A10: m = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; m = k + 1 by A10; hence F . 0 c= F . m by A9, A4; ::_thesis: verum end; A11: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A12: for m being Element of NAT st n < m holds F . n c= F . m ; ::_thesis: S1[n + 1] let m be Element of NAT ; ::_thesis: ( n + 1 < m implies F . (n + 1) c= F . m ) assume A13: n + 1 < m ; ::_thesis: F . (n + 1) c= F . m let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in F . (n + 1) or r in F . m ) A14: ( r in F . n implies r in F . m ) proof assume A15: r in F . n ; ::_thesis: r in F . m ( n < m implies r in F . m ) proof assume n < m ; ::_thesis: r in F . m then F . n c= F . m by A12; hence r in F . m by A15; ::_thesis: verum end; hence r in F . m by A13, NAT_1:13; ::_thesis: verum end; assume A16: r in F . (n + 1) ; ::_thesis: r in F . m A17: F . (n + 1) = (N . (n + 1)) \/ (F . n) by A2; ( r in N . (n + 1) implies r in F . m ) by A1, A2, A13, Th5; hence r in F . m by A16, A17, A14, XBOOLE_0:def_3; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A11); ::_thesis: verum end; theorem Th7: :: MEASURE2:7 for X being set for S being non empty Subset-Family of X for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n <= m holds F . n c= G . m proof let X be set ; ::_thesis: for S being non empty Subset-Family of X for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n <= m holds F . n c= G . m let S be non empty Subset-Family of X; ::_thesis: for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n <= m holds F . n c= G . m let N, G, F be Function of NAT,S; ::_thesis: ( 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 Element of NAT st n <= m holds F . n c= G . m ) assume that A1: G . 0 = N . 0 and A2: for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) and A3: F . 0 = N . 0 and A4: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: for n, m being Element of NAT st n <= m holds F . n c= G . m let n, m be Element of NAT ; ::_thesis: ( n <= m implies F . n c= G . m ) A5: for n being Element of NAT holds F . n c= G . n proof defpred S1[ Element of NAT ] means F . \$1 c= G . \$1; A6: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume F . n c= G . n ; ::_thesis: S1[n + 1] G . (n + 1) = (N . (n + 1)) \/ (G . n) by A2; then A7: N . (n + 1) c= G . (n + 1) by XBOOLE_1:7; F . (n + 1) = (N . (n + 1)) \ (G . n) by A4; hence S1[n + 1] by A7, XBOOLE_1:1; ::_thesis: verum end; A8: S1[ 0 ] by A1, A3; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A6); ::_thesis: verum end; A9: ( n < m implies F . n c= G . m ) proof assume n < m ; ::_thesis: F . n c= G . m then A10: G . n c= G . m by A1, A2, Th6; F . n c= G . n by A5; hence F . n c= G . m by A10, XBOOLE_1:1; ::_thesis: verum end; assume n <= m ; ::_thesis: F . n c= G . m then ( n = m or n < m ) by XXREAL_0:1; hence F . n c= G . m by A5, A9; ::_thesis: verum end; theorem Th8: :: MEASURE2:8 for X being set for S being SigmaField of X for N, G being Function of NAT,S 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 X be set ; ::_thesis: for S being SigmaField of X for N, G being Function of NAT,S 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) ) ) let S be SigmaField of X; ::_thesis: for N, G being Function of NAT,S 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) ) ) let N, G be Function of NAT,S; ::_thesis: 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) ) ) defpred S1[ set , set , set ] means for A, B being Element of S for c being Element of NAT st c = \$1 & A = \$2 & B = \$3 holds B = (N . (c + 1)) \ (G . c); A1: for c being Element of NAT for A being Element of S ex B being Element of S st S1[c,A,B] proof let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B] let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B] consider B being set such that A2: B = (N . (c + 1)) \ (G . c) ; reconsider B = B as Element of S by A2; take B ; ::_thesis: S1[c,A,B] thus S1[c,A,B] by A2; ::_thesis: verum end; consider F being Function of NAT,S such that A3: ( F . 0 = N . 0 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) proof let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . (n + 1)) \ (G . n) for a, b being Element of S for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds b = (N . (s + 1)) \ (G . s) by A3; hence F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: verum end; hence 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) ) ) by A3; ::_thesis: verum end; theorem :: MEASURE2:9 for X being set for S being SigmaField of X for N being Function of NAT,S 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 X be set ; ::_thesis: for S being SigmaField of X for N being Function of NAT,S ex F being Function of NAT,S st ( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) ) let S be SigmaField of X; ::_thesis: for N being Function of NAT,S ex F being Function of NAT,S st ( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) ) let N be Function of NAT,S; ::_thesis: ex F being Function of NAT,S st ( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) ) defpred S1[ set , set , set ] means for A, B being Element of S for c being Element of NAT st c = \$1 & A = \$2 & B = \$3 holds B = (N . 0) \ (N . c); reconsider A = {} as Element of S by PROB_1:4; A1: for c being Element of NAT for A being Element of S ex B being Element of S st S1[c,A,B] proof let c be Element of NAT ; ::_thesis: for A being Element of S ex B being Element of S st S1[c,A,B] let A be Element of S; ::_thesis: ex B being Element of S st S1[c,A,B] reconsider B = (N . 0) \ (N . c) as Element of S ; take B ; ::_thesis: S1[c,A,B] thus S1[c,A,B] ; ::_thesis: verum end; consider F being Function of NAT,S such that A2: ( F . 0 = A & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) proof let n be Element of NAT ; ::_thesis: F . (n + 1) = (N . 0) \ (N . n) for a, b being Element of S for s being Element of NAT st s = n & a = F . n & b = F . (n + 1) holds b = (N . 0) \ (N . s) by A2; hence F . (n + 1) = (N . 0) \ (N . n) ; ::_thesis: verum end; hence ex F being Function of NAT,S st ( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) ) by A2; ::_thesis: verum end; theorem Th10: :: MEASURE2:10 for X being set for S being SigmaField of X for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n < m holds F . n misses F . m proof let X be set ; ::_thesis: for S being SigmaField of X for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n < m holds F . n misses F . m let S be SigmaField of X; ::_thesis: for N, G, F being Function of NAT,S st 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) ) holds for n, m being Element of NAT st n < m holds F . n misses F . m let N, G, F be Function of NAT,S; ::_thesis: ( 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 Element of NAT st n < m holds F . n misses F . m ) assume that A1: ( G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 ) and A2: for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ; ::_thesis: for n, m being Element of NAT st n < m holds F . n misses F . m let n, m be Element of NAT ; ::_thesis: ( n < m implies F . n misses F . m ) assume A3: n < m ; ::_thesis: F . n misses F . m then 0 <> m by NAT_1:2; then consider k being Nat such that A4: m = k + 1 by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; F . (k + 1) = (N . (k + 1)) \ (G . k) by A2; then A5: G . k misses F . (k + 1) by XBOOLE_1:79; n <= k by A3, A4, NAT_1:13; hence (F . n) /\ (F . m) = ((F . n) /\ (G . k)) /\ (F . (k + 1)) by A1, A2, A4, Th7, XBOOLE_1:28 .= (F . n) /\ ((G . k) /\ (F . (k + 1))) by XBOOLE_1:16 .= (F . n) /\ {} by A5, XBOOLE_0:def_7 .= {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; theorem Th11: :: MEASURE2:11 for X being set for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S for F being Function of NAT,S st T = rng F holds M . (union T) <= SUM (M * F) proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S for F being Function of NAT,S st T = rng F holds M . (union T) <= SUM (M * F) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for T being N_Measure_fam of S for F being Function of NAT,S st T = rng F holds M . (union T) <= SUM (M * F) let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S for F being Function of NAT,S st T = rng F holds M . (union T) <= SUM (M * F) let T be N_Measure_fam of S; ::_thesis: for F being Function of NAT,S st T = rng F holds M . (union T) <= SUM (M * F) let F be Function of NAT,S; ::_thesis: ( T = rng F implies M . (union T) <= SUM (M * F) ) consider G being Function of NAT,S such that A1: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) ) by Th4; consider H being Function of NAT,S such that A2: H . 0 = F . 0 and A3: for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) by Th8; for n, m being set st n <> m holds H . n misses H . m proof let n, m be set ; ::_thesis: ( n <> m implies H . n misses H . m ) assume A4: n <> m ; ::_thesis: H . n misses H . m percases ( ( n in dom H & m in dom H ) or not n in dom H or not m in dom H ) ; suppose ( n in dom H & m in dom H ) ; ::_thesis: H . n misses H . m then reconsider n9 = n, m9 = m as Element of NAT ; A5: ( m9 < n9 implies H . m misses H . n ) by A1, A2, A3, Th10; ( n9 < m9 implies H . n misses H . m ) by A1, A2, A3, Th10; hence H . n misses H . m by A4, A5, XXREAL_0:1; ::_thesis: verum end; suppose ( not n in dom H or not m in dom H ) ; ::_thesis: H . n misses H . m then ( H . n = {} or H . m = {} ) by FUNCT_1:def_2; hence H . n misses H . m by XBOOLE_1:65; ::_thesis: verum end; end; end; then H is Sep_Sequence of S by PROB_2:def_2; then A6: SUM (M * H) = M . (union (rng H)) by MEASURE1:def_6; A7: for n being Element of NAT holds H . n c= F . n proof let n be Element of NAT ; ::_thesis: H . n c= F . n A8: ( ex k being Nat st n = k + 1 implies H . n c= F . n ) proof given k being Nat such that A9: n = k + 1 ; ::_thesis: H . n c= F . n reconsider k = k as Element of NAT by ORDINAL1:def_12; H . n = (F . n) \ (G . k) by A3, A9; hence H . n c= F . n by XBOOLE_1:36; ::_thesis: verum end; ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6; hence H . n c= F . n by A2, A8; ::_thesis: verum end; A10: for n being Element of NAT holds (M * H) . n <= (M * F) . n proof let n be Element of NAT ; ::_thesis: (M * H) . n <= (M * F) . n NAT = dom (M * F) by FUNCT_2:def_1; then A11: (M * F) . n = M . (F . n) by FUNCT_1:12; NAT = dom (M * H) by FUNCT_2:def_1; then (M * H) . n = M . (H . n) by FUNCT_1:12; hence (M * H) . n <= (M * F) . n by A7, A11, MEASURE1:31; ::_thesis: verum end; A12: union (rng H) = union (rng F) proof thus union (rng H) c= union (rng F) :: according to XBOOLE_0:def_10 ::_thesis: union (rng F) c= union (rng H) proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng H) or r in union (rng F) ) assume r in union (rng H) ; ::_thesis: r in union (rng F) then consider E being set such that A13: r in E and A14: E in rng H by TARSKI:def_4; consider s being set such that A15: s in dom H and A16: E = H . s by A14, FUNCT_1:def_3; reconsider s = s as Element of NAT by A15; A17: F . s in rng F by FUNCT_2:4; E c= F . s by A7, A16; hence r in union (rng F) by A13, A17, TARSKI:def_4; ::_thesis: verum end; let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng F) or r in union (rng H) ) assume r in union (rng F) ; ::_thesis: r in union (rng H) then consider E being set such that A18: r in E and A19: E in rng F by TARSKI:def_4; A20: ex s being set st ( s in dom F & E = F . s ) by A19, FUNCT_1:def_3; ex s1 being Element of NAT st r in H . s1 proof defpred S1[ Nat] means r in F . \$1; A21: ex k being Nat st S1[k] by A18, A20; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A21); then consider k being Nat such that A22: r in F . k and A23: for n being Nat st r in F . n holds k <= n ; A24: ( 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 A25: k = l + 1 ; ::_thesis: ex s1 being Element of NAT st r in H . s1 take k ; ::_thesis: ( k is Element of REAL & k is Element of NAT & r in H . k ) reconsider l = l as Element of NAT by ORDINAL1:def_12; A26: not r in G . l proof assume r in G . l ; ::_thesis: contradiction then consider i being Element of NAT such that A27: i <= l and A28: r in F . i by A1, Th5; k <= i by A23, A28; hence contradiction by A25, A27, NAT_1:13; ::_thesis: verum end; H . (l + 1) = (F . (l + 1)) \ (G . l) by A3; hence ( k is Element of REAL & k is Element of NAT & r in H . k ) by A22, A25, A26, XBOOLE_0:def_5; ::_thesis: verum end; ( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A2, A22; hence ex s1 being Element of NAT st r in H . s1 by A24, NAT_1:6; ::_thesis: verum end; then consider s1 being Element of NAT such that A29: r in H . s1 ; H . s1 in rng H by FUNCT_2:4; hence r in union (rng H) by A29, TARSKI:def_4; ::_thesis: verum end; assume T = rng F ; ::_thesis: M . (union T) <= SUM (M * F) hence M . (union T) <= SUM (M * F) by A10, A6, A12, SUPINF_2:43; ::_thesis: verum end; theorem Th12: :: MEASURE2:12 for X being set for S being SigmaField of X for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F proof let X be set ; ::_thesis: for S being SigmaField of X for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F let S be SigmaField of X; ::_thesis: for T being N_Measure_fam of S ex F being Function of NAT,S st T = rng F let T be N_Measure_fam of S; ::_thesis: ex F being Function of NAT,S st T = rng F consider F being Function of NAT,(bool X) such that A1: T = rng F by SUPINF_2:def_8; rng F c= S by A1, Def1; then F is Function of NAT,S by FUNCT_2:6; then consider F being Function of NAT,S such that A2: T = rng F by A1; take F ; ::_thesis: T = rng F thus T = rng F by A2; ::_thesis: verum end; theorem Th13: :: MEASURE2:13 for N, F being Function 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 N, F be Function; ::_thesis: ( F . 0 = {} & ( for n being Element of NAT holds ( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) implies for n being Element of NAT holds F . n c= F . (n + 1) ) assume that A1: F . 0 = {} and A2: for n being Element of NAT holds ( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ; ::_thesis: for n being Element of NAT holds F . n c= F . (n + 1) defpred S1[ Element of NAT ] means F . \$1 c= F . (\$1 + 1); A3: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume F . n c= F . (n + 1) ; ::_thesis: S1[n + 1] F . ((n + 1) + 1) = (N . 0) \ (N . (n + 1)) by A2; then (N . 0) \ (N . n) c= F . ((n + 1) + 1) by A2, XBOOLE_1:34; hence S1[n + 1] by A2; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: F . n c= F . (n + 1) F . (0 + 1) = (N . 0) \ (N . 0) by A2; then A4: S1[ 0 ] by A1, XBOOLE_1:37; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); hence F . n c= F . (n + 1) ; ::_thesis: verum end; theorem :: MEASURE2:14 for X being set for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds union T is measure_zero of M proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds union T is measure_zero of M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds union T is measure_zero of M let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds union T is measure_zero of M let T be N_Measure_fam of S; ::_thesis: ( ( for A being set st A in T holds A is measure_zero of M ) implies union T is measure_zero of M ) consider F being Function of NAT,S such that A1: T = rng F by Th12; set G = M * F; assume A2: for A being set st A in T holds A is measure_zero of M ; ::_thesis: union T is measure_zero of M A3: for r being Element of NAT st 0 <= r holds (M * F) . r = 0. proof let r be Element of NAT ; ::_thesis: ( 0 <= r implies (M * F) . r = 0. ) F . r is measure_zero of M by A2, A1, FUNCT_2:4; then M . (F . r) = 0. by MEASURE1:def_7; hence ( 0 <= r implies (M * F) . r = 0. ) by FUNCT_2:15; ::_thesis: verum end; M * F is V86() by MEASURE1:25; then SUM (M * F) = (Ser (M * F)) . 0 by A3, SUPINF_2:48; then SUM (M * F) = (M * F) . 0 by SUPINF_2:44; then SUM (M * F) = 0. by A3; then A4: M . (union T) <= 0. by A1, Th11; 0. <= M . (union T) by MEASURE1:def_2; then M . (union T) = 0. by A4, XXREAL_0:1; hence union T is measure_zero of M by MEASURE1:def_7; ::_thesis: verum end; theorem :: MEASURE2:15 for X being set for S being SigmaField of X for M being sigma_Measure of S for 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 by MEASURE1:36, SETFAM_1:3; theorem :: MEASURE2:16 for X being set for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds meet T is measure_zero of M proof let X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds meet T is measure_zero of M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds meet T is measure_zero of M let M be sigma_Measure of S; ::_thesis: for T being N_Measure_fam of S st ( for A being set st A in T holds A is measure_zero of M ) holds meet T is measure_zero of M let T be N_Measure_fam of S; ::_thesis: ( ( for A being set st A in T holds A is measure_zero of M ) implies meet T is measure_zero of M ) assume A1: for A being set st A in T holds A is measure_zero of M ; ::_thesis: meet T 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_8; take F . 0 ; ::_thesis: ( F . 0 in T & F . 0 is measure_zero of M ) thus ( F . 0 in T & F . 0 is measure_zero of M ) by A1, A2, FUNCT_2:4; ::_thesis: verum end; hence meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3; ::_thesis: verum end; definition let X be set ; let S be SigmaField of X; let IT be N_Measure_fam of S; attrIT is non-decreasing means :Def2: :: MEASURE2:def 2 ex F being Function of NAT,S st ( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ); end; :: deftheorem Def2 defines non-decreasing MEASURE2:def_2_:_ for X being set for S being SigmaField of X for IT being N_Measure_fam of S holds ( IT is non-decreasing iff ex F being Function of NAT,S st ( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) ); registration let X be set ; let S be SigmaField of X; cluster non empty V46() non-decreasing for N_Measure_fam of S; existence ex b1 being N_Measure_fam of S st b1 is non-decreasing proof consider A being set such that A1: A in S by PROB_1:4; reconsider A = A as Subset of X by A1; consider B, C being Subset of X such that A2: ( B = A & C = A ) ; A3: {A} c= S by A1, ZFMISC_1:31; consider F being Function of NAT,(bool X) such that A4: rng F = {B,C} and A5: ( F . 0 = B & ( for n being Element of NAT st 0 < n holds F . n = C ) ) by MEASURE1:19; A6: rng F = {A} by A2, A4, ENUMSET1:29; then A7: rng F c= S by A1, ZFMISC_1:31; {A} is N_Sub_set_fam of X by A6, SUPINF_2:def_8; then reconsider T = {A} as N_Measure_fam of S by A3, Def1; reconsider F = F as Function of NAT,S by A7, FUNCT_2:6; take T ; ::_thesis: T is non-decreasing take F ; :: according to MEASURE2:def_2 ::_thesis: ( T = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) for n being Element of NAT holds F . n c= F . (n + 1) proof let n be Element of NAT ; ::_thesis: F . n c= F . (n + 1) F . n = A by A2, A5, NAT_1:3; hence F . n c= F . (n + 1) by A2, A5, NAT_1:3; ::_thesis: verum end; hence ( T = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) by A2, A4, ENUMSET1:29; ::_thesis: verum end; end; definition let X be set ; let S be SigmaField of X; let IT be N_Measure_fam of S; attrIT is non-increasing means :: MEASURE2:def 3 ex F being Function of NAT,S st ( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ); end; :: deftheorem defines non-increasing MEASURE2:def_3_:_ for X being set for S being SigmaField of X for IT being N_Measure_fam of S holds ( IT is non-increasing iff ex F being Function of NAT,S st ( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) ); registration let X be set ; let S be SigmaField of X; cluster non empty V46() non-increasing for N_Measure_fam of S; existence ex b1 being N_Measure_fam of S st b1 is non-increasing proof consider A being set such that A1: A in S by PROB_1:4; reconsider A = A as Subset of X by A1; A2: {A} c= S by A1, ZFMISC_1:31; set B = A; set C = A; consider F being Function of NAT,(bool X) such that A3: rng F = {A,A} and A4: ( F . 0 = A & ( for n being Element of NAT st 0 < n holds F . n = A ) ) by MEASURE1:19; A5: rng F = {A} by A3, ENUMSET1:29; then A6: rng F c= S by A1, ZFMISC_1:31; {A} is N_Sub_set_fam of X by A5, SUPINF_2:def_8; then reconsider T = {A} as N_Measure_fam of S by A2, Def1; reconsider F = F as Function of NAT,S by A6, FUNCT_2:6; take T ; ::_thesis: T is non-increasing take F ; :: according to MEASURE2:def_3 ::_thesis: ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) for n being Element of NAT holds F . (n + 1) c= F . n proof let n be Element of NAT ; ::_thesis: F . (n + 1) c= F . n F . n = A by A4, NAT_1:3; hence F . (n + 1) c= F . n by A4, NAT_1:3; ::_thesis: verum end; hence ( T = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) by A3, ENUMSET1:29; ::_thesis: verum end; end; theorem :: MEASURE2:17 for X being set for S being SigmaField of X for 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 rng F is non-decreasing N_Measure_fam of S proof let X be set ; ::_thesis: for S being SigmaField of X for 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 rng F is non-decreasing N_Measure_fam of S let S be SigmaField of X; ::_thesis: for 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 rng F is non-decreasing N_Measure_fam of S let N, F be Function of NAT,S; ::_thesis: ( 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 ) assume ( F . 0 = {} & ( for n being Element of NAT holds ( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) ) ; ::_thesis: rng F is non-decreasing N_Measure_fam of S then A1: for n being Element of NAT holds F . n c= F . (n + 1) by Th13; ( rng F c= S & rng F is N_Sub_set_fam of X ) by MEASURE1:23, RELAT_1:def_19; hence rng F is non-decreasing N_Measure_fam of S by A1, Def1, Def2; ::_thesis: verum end; theorem Th18: :: MEASURE2:18 for N being Function st ( for n being Element of NAT holds N . n c= N . (n + 1) ) holds for m, n being Element of NAT st n <= m holds N . n c= N . m proof let N be Function; ::_thesis: ( ( for n being Element of NAT holds N . n c= N . (n + 1) ) implies for m, n being Element of NAT st n <= m holds N . n c= N . m ) defpred S1[ Element of NAT ] means for n being Element of NAT st n <= \$1 holds N . n c= N . \$1; assume A1: for n being Element of NAT holds N . n c= N . (n + 1) ; ::_thesis: for m, n being Element of NAT st n <= m holds N . n c= N . m A2: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A3: for n being Element of NAT st n <= m holds N . n c= N . m ; ::_thesis: S1[m + 1] let n be Element of NAT ; ::_thesis: ( n <= m + 1 implies N . n c= N . (m + 1) ) A4: ( n <= m implies N . n c= N . (m + 1) ) proof assume n <= m ; ::_thesis: N . n c= N . (m + 1) then A5: N . n c= N . m by A3; N . m c= N . (m + 1) by A1; hence N . n c= N . (m + 1) by A5, XBOOLE_1:1; ::_thesis: verum end; assume n <= m + 1 ; ::_thesis: N . n c= N . (m + 1) hence N . n c= N . (m + 1) by A4, NAT_1:8; ::_thesis: verum end; A6: S1[ 0 ] by NAT_1:3; thus for m being Element of NAT holds S1[m] from NAT_1:sch_1(A6, A2); ::_thesis: verum end; theorem Th19: :: MEASURE2:19 for N, F being Function st 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) ) ) holds for n, m being Element of NAT st n < m holds F . n misses F . m proof let N, F be Function; ::_thesis: ( 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 Element of NAT st n < m holds F . n misses F . m ) assume that A1: F . 0 = N . 0 and A2: for n being Element of NAT holds ( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: for n, m being Element of NAT st n < m holds F . n misses F . m let n, m be Element of NAT ; ::_thesis: ( n < m implies F . n misses F . m ) assume A3: n < m ; ::_thesis: F . n misses F . m then 0 <> m by NAT_1:2; then consider k being Nat such that A4: m = k + 1 by NAT_1:6; A5: for n being Element of NAT holds F . n c= N . n proof defpred S1[ Element of NAT ] means F . \$1 c= N . \$1; A6: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume F . n c= N . n ; ::_thesis: S1[n + 1] F . (n + 1) = (N . (n + 1)) \ (N . n) by A2; hence S1[n + 1] ; ::_thesis: verum end; A7: S1[ 0 ] by A1; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); ::_thesis: verum end; A8: for n, m being Element of NAT st n <= m holds F . n c= N . m proof let n, m be Element of NAT ; ::_thesis: ( n <= m implies F . n c= N . m ) A9: ( n < m implies F . n c= N . m ) proof assume n < m ; ::_thesis: F . n c= N . m then A10: N . n c= N . m by A2, Th18; F . n c= N . n by A5; hence F . n c= N . m by A10, XBOOLE_1:1; ::_thesis: verum end; assume n <= m ; ::_thesis: F . n c= N . m then ( n = m or n < m ) by XXREAL_0:1; hence F . n c= N . m by A5, A9; ::_thesis: verum end; reconsider k = k as Element of NAT by ORDINAL1:def_12; F . (k + 1) = (N . (k + 1)) \ (N . k) by A2; then A11: N . k misses F . (k + 1) by XBOOLE_1:79; n <= k by A3, A4, NAT_1:13; then (F . n) /\ (F . (k + 1)) = ((F . n) /\ (N . k)) /\ (F . (k + 1)) by A8, XBOOLE_1:28 .= (F . n) /\ ((N . k) /\ (F . (k + 1))) by XBOOLE_1:16 .= (F . n) /\ {} by A11, XBOOLE_0:def_7 .= {} ; hence F . n misses F . m by A4, XBOOLE_0:def_7; ::_thesis: verum end; theorem Th20: :: MEASURE2:20 for X being set for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds union (rng F) = union (rng N) proof let X be set ; ::_thesis: for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds union (rng F) = union (rng N) let S be SigmaField of X; ::_thesis: for N, 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) & N . n c= N . (n + 1) ) ) holds union (rng F) = union (rng N) let N, F be Function of NAT,S; ::_thesis: ( 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) ) assume that A1: F . 0 = N . 0 and A2: for n being Element of NAT holds ( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: union (rng F) = union (rng N) thus union (rng F) c= union (rng N) :: according to XBOOLE_0:def_10 ::_thesis: union (rng N) c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng F) or x in union (rng N) ) assume x in union (rng F) ; ::_thesis: x in union (rng N) then consider Y being set such that A3: x in Y and A4: Y in rng F by TARSKI:def_4; consider n being set such that A5: n in dom F and A6: Y = F . n by A4, FUNCT_1:def_3; reconsider n = n as Element of NAT by A5; A7: ( 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 A8: n = k + 1 ; ::_thesis: ex Z being set st ( x in Z & Z in rng N ) reconsider k = k as Element of NAT by ORDINAL1:def_12; Y = (N . (k + 1)) \ (N . k) by A2, A6, A8; then x in N . (k + 1) by A3, XBOOLE_0:def_5; hence ex Z being set st ( x in Z & Z in rng N ) by FUNCT_2:4; ::_thesis: verum end; ( n = 0 implies ex Z being set st ( x in Z & Z in rng N ) ) by A1, A3, A6, FUNCT_2:4; hence x in union (rng N) by A7, NAT_1:6, TARSKI:def_4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng N) or x in union (rng F) ) assume x in union (rng N) ; ::_thesis: x in union (rng F) then consider Y being set such that A9: x in Y and A10: Y in rng N by TARSKI:def_4; A11: ex n being set st ( n in dom N & Y = N . n ) by A10, FUNCT_1:def_3; 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 S1[ Nat] means x in N . \$1; A12: ex k being Nat st S1[k] by A9, A11; ex k being Nat st ( S1[k] & ( for r being Nat st S1[r] holds k <= r ) ) from NAT_1:sch_5(A12); then consider k being Nat such that A13: x in N . k and A14: for r being Nat st x in N . r holds k <= r ; A15: ( 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 A16: k = l + 1 ; ::_thesis: ex s being Element of NAT st x in F . s take k ; ::_thesis: ( k is Element of REAL & k is Element of NAT & x in F . k ) reconsider l = l as Element of NAT by ORDINAL1:def_12; A17: not x in N . l proof assume x in N . l ; ::_thesis: contradiction then l + 1 <= l by A14, A16; hence contradiction by NAT_1:13; ::_thesis: verum end; F . (l + 1) = (N . (l + 1)) \ (N . l) by A2; hence ( k is Element of REAL & k is Element of NAT & x in F . k ) by A13, A16, A17, XBOOLE_0:def_5; ::_thesis: verum end; ( k = 0 implies ex s being Element of NAT st x in F . s ) by A1, A13; hence ex s being Element of NAT st x in F . s by A15, NAT_1:6; ::_thesis: verum end; hence ex Z being set st ( x in Z & Z in rng F ) by FUNCT_2:4; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; theorem Th21: :: MEASURE2:21 for X being set for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds F is Sep_Sequence of S proof let X be set ; ::_thesis: for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds F is Sep_Sequence of S let S be SigmaField of X; ::_thesis: for N, 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) & N . n c= N . (n + 1) ) ) holds F is Sep_Sequence of S let N, F be Function of NAT,S; ::_thesis: ( 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 ) 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) ) ) ) ; ::_thesis: F is Sep_Sequence of S for n, m being set st n <> m holds F . n misses F . m proof let n, m be set ; ::_thesis: ( n <> m implies F . n misses F . m ) assume A2: n <> m ; ::_thesis: F . n misses F . m percases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ; suppose ( n in dom F & m in dom F ) ; ::_thesis: F . n misses F . m then reconsider n9 = n, m9 = m as Element of NAT ; A3: ( m9 < n9 implies F . m misses F . n ) by A1, Th19; ( n9 < m9 implies F . n misses F . m ) by A1, Th19; hence F . n misses F . m by A2, A3, XXREAL_0:1; ::_thesis: verum end; suppose ( not n in dom F or not m in dom F ) ; ::_thesis: F . n misses F . m then ( F . n = {} or F . m = {} ) by FUNCT_1:def_2; hence F . n misses F . m by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F is Sep_Sequence of S by PROB_2:def_2; ::_thesis: verum end; theorem :: MEASURE2:22 for X being set for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) proof let X be set ; ::_thesis: for S being SigmaField of X for N, 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) & N . n c= N . (n + 1) ) ) holds ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) let S be SigmaField of X; ::_thesis: for N, 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) & N . n c= N . (n + 1) ) ) holds ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) let N, F be Function of NAT,S; ::_thesis: ( 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) ) ) ) assume that A1: F . 0 = N . 0 and A2: for n being Element of NAT holds ( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ; ::_thesis: ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) proof let n be Element of NAT ; ::_thesis: N . (n + 1) = (F . (n + 1)) \/ (N . n) F . (n + 1) = (N . (n + 1)) \ (N . n) by A2; hence N . (n + 1) = (F . (n + 1)) \/ (N . n) by A2, XBOOLE_1:45; ::_thesis: verum end; hence ( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) ) by A1; ::_thesis: verum end; theorem :: MEASURE2:23 for X being set for S being SigmaField of X for M being sigma_Measure of S for 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 X be set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for 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)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for 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)) let M be sigma_Measure of S; ::_thesis: for 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)) let F be Function of NAT,S; ::_thesis: ( ( for n being Element of NAT holds F . n c= F . (n + 1) ) implies M . (union (rng F)) = sup (rng (M * F)) ) consider G being Function of NAT,S such that A1: G . 0 = F . 0 and A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \ (F . n) by Th3; assume A3: for n being Element of NAT holds F . n c= F . (n + 1) ; ::_thesis: M . (union (rng F)) = sup (rng (M * F)) then A4: G is Sep_Sequence of S by A1, A2, Th21; A5: for m being set st m in NAT holds (Ser (M * G)) . m = (M * F) . m proof defpred S1[ Element of NAT ] means (Ser (M * G)) . \$1 = (M * F) . \$1; let m be set ; ::_thesis: ( m in NAT implies (Ser (M * G)) . m = (M * F) . m ) assume A6: m in NAT ; ::_thesis: (Ser (M * G)) . m = (M * F) . m A7: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) A8: (M * G) . (m + 1) = M . (G . (m + 1)) by FUNCT_2:15; A9: (M * F) . (m + 1) = M . (F . (m + 1)) by FUNCT_2:15; A10: G . (m + 1) = (F . (m + 1)) \ (F . m) by A2; assume (Ser (M * G)) . m = (M * F) . m ; ::_thesis: S1[m + 1] then (Ser (M * G)) . (m + 1) = ((M * F) . m) + ((M * G) . (m + 1)) by SUPINF_2:44 .= (M . (F . m)) + (M . (G . (m + 1))) by A8, FUNCT_2:15 .= M . ((F . m) \/ (G . (m + 1))) by A10, MEASURE1:30, XBOOLE_1:79 .= (M * F) . (m + 1) by A3, A9, A10, XBOOLE_1:45 ; hence S1[m + 1] ; ::_thesis: verum end; (Ser (M * G)) . 0 = (M * G) . 0 by SUPINF_2:44 .= M . (F . 0) by A1, FUNCT_2:15 .= (M * F) . 0 by FUNCT_2:15 ; then A11: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A11, A7); hence (Ser (M * G)) . m = (M * F) . m by A6; ::_thesis: verum end; A12: ( dom (Ser (M * G)) = NAT & dom (M * F) = NAT ) by FUNCT_2:def_1; M . (union (rng F)) = M . (union (rng G)) by A3, A1, A2, Th20 .= SUM (M * G) by A4, MEASURE1:def_6 .= sup (rng (M * F)) by A12, A5, FUNCT_1:2 ; hence M . (union (rng F)) = sup (rng (M * F)) ; ::_thesis: verum end;