:: MEASURE4 semantic presentation begin theorem Th1: :: MEASURE4:1 for X being set for S being non empty Subset-Family of X for F, G being Function of NAT,S for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds union (rng G) = A /\ (union (rng F)) proof let X be set ; ::_thesis: for S being non empty Subset-Family of X for F, G being Function of NAT,S for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds union (rng G) = A /\ (union (rng F)) let S be non empty Subset-Family of X; ::_thesis: for F, G being Function of NAT,S for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds union (rng G) = A /\ (union (rng F)) let F, G be Function of NAT,S; ::_thesis: for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds union (rng G) = A /\ (union (rng F)) let A be Element of S; ::_thesis: ( ( for n being Element of NAT holds G . n = A /\ (F . n) ) implies union (rng G) = A /\ (union (rng F)) ) assume A1: for n being Element of NAT holds G . n = A /\ (F . n) ; ::_thesis: union (rng G) = A /\ (union (rng F)) thus union (rng G) c= A /\ (union (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (union (rng F)) c= union (rng G) proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng G) or r in A /\ (union (rng F)) ) assume r in union (rng G) ; ::_thesis: r in A /\ (union (rng F)) then consider E being set such that A2: r in E and A3: E in rng G by TARSKI:def_4; consider s being set such that A4: s in dom G and A5: E = G . s by A3, FUNCT_1:def_3; reconsider s = s as Element of NAT by A4; A6: r in A /\ (F . s) by A1, A2, A5; then A7: r in A by XBOOLE_0:def_4; A8: F . s in rng F by FUNCT_2:4; r in F . s by A6, XBOOLE_0:def_4; then r in union (rng F) by A8, TARSKI:def_4; hence r in A /\ (union (rng F)) by A7, XBOOLE_0:def_4; ::_thesis: verum end; let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in A /\ (union (rng F)) or r in union (rng G) ) assume A9: r in A /\ (union (rng F)) ; ::_thesis: r in union (rng G) then A10: r in A by XBOOLE_0:def_4; r in union (rng F) by A9, XBOOLE_0:def_4; then consider E being set such that A11: r in E and A12: E in rng F by TARSKI:def_4; consider s being set such that A13: s in dom F and A14: E = F . s by A12, FUNCT_1:def_3; reconsider s = s as Element of NAT by A13; A15: G . s in rng G by FUNCT_2:4; A /\ E = G . s by A1, A14; then r in G . s by A10, A11, XBOOLE_0:def_4; hence r in union (rng G) by A15, TARSKI:def_4; ::_thesis: verum end; theorem Th2: :: MEASURE4:2 for X being set for S being non empty Subset-Family of X for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds union (rng F) = union (rng H) proof let X be set ; ::_thesis: for S being non empty Subset-Family of X for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds union (rng F) = union (rng H) let S be non empty Subset-Family of X; ::_thesis: for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds union (rng F) = union (rng H) let F, G be Function of NAT,S; ::_thesis: ( G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) implies for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds union (rng F) = union (rng H) ) assume that A1: G . 0 = F . 0 and A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ; ::_thesis: for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds union (rng F) = union (rng H) let H be Function of NAT,S; ::_thesis: ( H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) implies union (rng F) = union (rng H) ) assume that A3: H . 0 = F . 0 and A4: for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ; ::_thesis: union (rng F) = union (rng H) thus union (rng F) c= union (rng H) :: according to XBOOLE_0:def_10 ::_thesis: union (rng H) c= union (rng F) proof 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 A5: r in E and A6: E in rng F by TARSKI:def_4; A7: ex s being set st ( s in dom F & E = F . s ) by A6, FUNCT_1:def_3; ex s1 being Element of NAT st r in H . s1 proof defpred S1[ Nat] means r in F . \$1; A8: ex k being Nat st S1[k] by A5, A7; ex k being Nat st ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A8); then consider k being Nat such that A9: r in F . k and A10: for n being Nat st r in F . n holds k <= n ; A11: ( 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 A12: 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; A13: not r in G . l proof assume r in G . l ; ::_thesis: contradiction then consider i being Element of NAT such that A14: i <= l and A15: r in F . i by A1, A2, MEASURE2:5; k <= i by A10, A15; hence contradiction by A12, A14, NAT_1:13; ::_thesis: verum end; H . (l + 1) = (F . (l + 1)) \ (G . l) by A4; hence ( k is Element of REAL & k is Element of NAT & r in H . k ) by A9, A12, A13, XBOOLE_0:def_5; ::_thesis: verum end; ( k = 0 implies ex s1 being Element of NAT st r in H . s1 ) by A3, A9; hence ex s1 being Element of NAT st r in H . s1 by A11, NAT_1:6; ::_thesis: verum end; then consider s1 being Element of NAT such that A16: r in H . s1 ; H . s1 in rng H by FUNCT_2:4; hence r in union (rng H) by A16, TARSKI:def_4; ::_thesis: verum end; A17: 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 A18: ( ex k being Nat st n = k + 1 implies H . n c= F . n ) proof given k being Nat such that A19: 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 A4, A19; hence H . n c= F . n ; ::_thesis: verum end; ( n = 0 implies H . n c= F . n ) by A3; hence H . n c= F . n by A18, NAT_1:6; ::_thesis: verum end; union (rng H) c= union (rng F) 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 A20: r in E and A21: E in rng H by TARSKI:def_4; consider s being set such that A22: s in dom H and A23: E = H . s by A21, FUNCT_1:def_3; reconsider s = s as Element of NAT by A22; A24: F . s in rng F by FUNCT_2:4; E c= F . s by A17, A23; hence r in union (rng F) by A20, A24, TARSKI:def_4; ::_thesis: verum end; hence union (rng H) c= union (rng F) ; ::_thesis: verum end; theorem Th3: :: MEASURE4:3 for X being set holds bool X is SigmaField of X proof let X be set ; ::_thesis: bool X is SigmaField of X A1: for M being N_Sub_set_fam of X st M c= bool X holds union M in bool X ; reconsider Y = bool X as Subset-Family of X ; for A being set st A in bool X holds X \ A in bool X ; then reconsider Y = Y as non empty compl-closed sigma-additive Subset-Family of X by A1, MEASURE1:def_1, MEASURE1:def_5; Y is SigmaField of X ; hence bool X is SigmaField of X ; ::_thesis: verum end; definition let X be set ; mode C_Measure of X -> Function of (bool X),ExtREAL means :Def1: :: MEASURE4:def 1 ( it is V87() & it is zeroed & ( for A, B being Subset of X st A c= B holds ( it . A <= it . B & ( for F being Function of NAT,(bool X) holds it . (union (rng F)) <= SUM (it * F) ) ) ) ); existence ex b1 being Function of (bool X),ExtREAL st ( b1 is V87() & b1 is zeroed & ( for A, B being Subset of X st A c= B holds ( b1 . A <= b1 . B & ( for F being Function of NAT,(bool X) holds b1 . (union (rng F)) <= SUM (b1 * F) ) ) ) ) proof set M = (bool X) --> 0.; take (bool X) --> 0. ; ::_thesis: ( (bool X) --> 0. is V87() & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds ( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) ) A1: for A being Subset of X holds 0. <= ((bool X) --> 0.) . A ; then A2: (bool X) --> 0. is V87() by MEASURE1:def_2; A3: for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) proof let F be Function of NAT,(bool X); ::_thesis: ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) A4: ((bool X) --> 0.) . (union (rng F)) = 0. by FUNCOP_1:7; A5: for r being Element of NAT st 0 <= r holds (((bool X) --> 0.) * F) . r = 0. proof let r be Element of NAT ; ::_thesis: ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. ) dom (((bool X) --> 0.) * F) = NAT by FUNCT_2:def_1; then (((bool X) --> 0.) * F) . r = ((bool X) --> 0.) . (F . r) by FUNCT_1:12; hence ( 0 <= r implies (((bool X) --> 0.) * F) . r = 0. ) by FUNCOP_1:7; ::_thesis: verum end; A6: (Ser (((bool X) --> 0.) * F)) . 0 = (((bool X) --> 0.) * F) . 0 by SUPINF_2:44; ((bool X) --> 0.) * F is V87() by A2, MEASURE1:25; hence ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) by A4, A5, A6, SUPINF_2:48; ::_thesis: verum end; {} c= X by XBOOLE_1:2; then ((bool X) --> 0.) . {} = 0. by FUNCOP_1:7; hence ( (bool X) --> 0. is V87() & (bool X) --> 0. is zeroed & ( for A, B being Subset of X st A c= B holds ( ((bool X) --> 0.) . A <= ((bool X) --> 0.) . B & ( for F being Function of NAT,(bool X) holds ((bool X) --> 0.) . (union (rng F)) <= SUM (((bool X) --> 0.) * F) ) ) ) ) by A1, A3, FUNCOP_1:7, MEASURE1:def_2, VALUED_0:def_19; ::_thesis: verum end; end; :: deftheorem Def1 defines C_Measure MEASURE4:def_1_:_ for X being set for b2 being Function of (bool X),ExtREAL holds ( b2 is C_Measure of X iff ( b2 is V87() & b2 is zeroed & ( for A, B being Subset of X st A c= B holds ( b2 . A <= b2 . B & ( for F being Function of NAT,(bool X) holds b2 . (union (rng F)) <= SUM (b2 * F) ) ) ) ) ); definition let X be set ; let C be C_Measure of X; func sigma_Field C -> non empty Subset-Family of X means :Def2: :: MEASURE4:def 2 for A being Subset of X holds ( A in it iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ); existence ex b1 being non empty Subset-Family of X st for A being Subset of X holds ( A in b1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) proof reconsider A = {} as Subset of X by XBOOLE_1:2; defpred S1[ set ] means for A being set st A = \$1 holds for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z); consider D being set such that A1: for y being set holds ( y in D iff ( y in bool X & S1[y] ) ) from XBOOLE_0:sch_1(); A2: for A being set holds ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) ) proof let A be set ; ::_thesis: ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) ) ( S1[A] iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ; hence ( A in D iff ( A in bool X & ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) ) by A1; ::_thesis: verum end; then A3: for A being set st A in D holds A in bool X ; now__::_thesis:_for_W,_Z_being_Subset_of_X_st_W_c=_A_&_Z_c=_X_\_A_holds_ (C_._W)_+_(C_._Z)_<=_C_._(W_\/_Z) let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A4: W c= A and Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) A5: W = {} by A4; C is zeroed by Def1; then C . W = 0 by A5, VALUED_0:def_19; hence (C . W) + (C . Z) <= C . (W \/ Z) by A5, XXREAL_3:4; ::_thesis: verum end; then reconsider D = D as non empty Subset-Family of X by A2, A3, TARSKI:def_3; take D ; ::_thesis: for A being Subset of X holds ( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) thus for A being Subset of X holds ( A in D iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset-Family of X st ( for A being Subset of X holds ( A in b1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds ( A in b2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) holds b1 = b2 proof let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for A being Subset of X holds ( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds ( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ) implies D1 = D2 ) assume that A6: for A being Subset of X holds ( A in D1 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) and A7: for A being Subset of X holds ( A in D2 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ; ::_thesis: D1 = D2 for A being set holds ( A in D1 iff A in D2 ) proof let A be set ; ::_thesis: ( A in D1 iff A in D2 ) hereby ::_thesis: ( A in D2 implies A in D1 ) assume A8: A in D1 ; ::_thesis: A in D2 then reconsider A9 = A as Subset of X ; for W, Z being Subset of X st W c= A & Z c= X \ A9 holds (C . W) + (C . Z) <= C . (W \/ Z) by A6, A8; hence A in D2 by A7; ::_thesis: verum end; assume A9: A in D2 ; ::_thesis: A in D1 then reconsider A = A as Subset of X ; for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) by A7, A9; hence A in D1 by A6; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def2 defines sigma_Field MEASURE4:def_2_:_ for X being set for C being C_Measure of X for b3 being non empty Subset-Family of X holds ( b3 = sigma_Field C iff for A being Subset of X holds ( A in b3 iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ) ); theorem Th4: :: MEASURE4:4 for X being set for C being C_Measure of X for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z) proof let X be set ; ::_thesis: for C being C_Measure of X for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z) let C be C_Measure of X; ::_thesis: for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z) let W, Z be Subset of X; ::_thesis: C . (W \/ Z) <= (C . W) + (C . Z) reconsider P = {} as Subset of X by XBOOLE_1:2; consider F being Function of NAT,(bool X) such that A1: rng F = {W,Z,P} and A2: F . 0 = W and A3: F . 1 = Z and A4: for n being Element of NAT st 1 < n holds F . n = P by MEASURE1:17; A5: (C * F) . 1 = C . Z by A3, FUNCT_2:15; set G = C * F; A6: union {W,Z,P} = W \/ Z proof thus union {W,Z,P} c= W \/ Z :: according to XBOOLE_0:def_10 ::_thesis: W \/ Z c= union {W,Z,P} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union {W,Z,P} or x in W \/ Z ) assume x in union {W,Z,P} ; ::_thesis: x in W \/ Z then ex Y being set st ( x in Y & Y in {W,Z,P} ) by TARSKI:def_4; then ( x in W or x in Z or x in P ) by ENUMSET1:def_1; hence x in W \/ Z by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W \/ Z or x in union {W,Z,P} ) assume A7: x in W \/ Z ; ::_thesis: x in union {W,Z,P} now__::_thesis:_ex_Y_being_Subset_of_X_st_ (_x_in_Y_&_Y_in_{W,Z,P}_) percases ( x in W or x in Z ) by A7, XBOOLE_0:def_3; supposeA8: x in W ; ::_thesis: ex Y being Subset of X st ( x in Y & Y in {W,Z,P} ) take Y = W; ::_thesis: ( x in Y & Y in {W,Z,P} ) thus ( x in Y & Y in {W,Z,P} ) by A8, ENUMSET1:def_1; ::_thesis: verum end; supposeA9: x in Z ; ::_thesis: ex Y being Subset of X st ( x in Y & Y in {W,Z,P} ) take Y = Z; ::_thesis: ( x in Y & Y in {W,Z,P} ) thus ( x in Y & Y in {W,Z,P} ) by A9, ENUMSET1:def_1; ::_thesis: verum end; end; end; hence x in union {W,Z,P} by TARSKI:def_4; ::_thesis: verum end; A10: C is zeroed by Def1; A11: for r being Element of NAT st 2 <= r holds (C * F) . r = 0. proof let r be Element of NAT ; ::_thesis: ( 2 <= r implies (C * F) . r = 0. ) assume 2 <= r ; ::_thesis: (C * F) . r = 0. then 1 + 1 <= r ; then 1 < r by NAT_1:13; then A12: F . r = {} by A4; C is zeroed by Def1; then C . (F . r) = 0. by A12, VALUED_0:def_19; hence (C * F) . r = 0. by FUNCT_2:15; ::_thesis: verum end; C is V87() by Def1; then A13: C * F is V87() by MEASURE1:25; F . 2 = P by A4; then A14: (C * F) . 2 = C . P by FUNCT_2:15; A15: (C * F) . 0 = C . W by A2, FUNCT_2:15; consider y1, y2 being R_eal such that A16: y1 = (Ser (C * F)) . 1 and A17: y2 = (Ser (C * F)) . 0 ; (Ser (C * F)) . 2 = y1 + ((C * F) . (1 + 1)) by A16, SUPINF_2:44 .= ((Ser (C * F)) . 1) + 0. by A14, A16, A10, VALUED_0:def_19 .= (Ser (C * F)) . 1 by XXREAL_3:4 .= y2 + ((C * F) . (0 + 1)) by A17, SUPINF_2:44 .= (C . W) + (C . Z) by A5, A15, A17, SUPINF_2:44 ; then SUM (C * F) = (C . W) + (C . Z) by A13, A11, SUPINF_2:48; hence C . (W \/ Z) <= (C . W) + (C . Z) by A1, A6, Def1; ::_thesis: verum end; theorem Th5: :: MEASURE4:5 for X being set for C being C_Measure of X for A being Subset of X holds ( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ) proof let X be set ; ::_thesis: for C being C_Measure of X for A being Subset of X holds ( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ) let C be C_Measure of X; ::_thesis: for A being Subset of X holds ( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ) let A be Subset of X; ::_thesis: ( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ) hereby ::_thesis: ( ( for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ) implies A in sigma_Field C ) assume A1: A in sigma_Field C ; ::_thesis: for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) = C . (W \/ Z) ) assume that A2: W c= A and A3: Z c= X \ A ; ::_thesis: (C . W) + (C . Z) = C . (W \/ Z) A4: C . (W \/ Z) <= (C . W) + (C . Z) by Th4; (C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, A3, Def2; hence (C . W) + (C . Z) = C . (W \/ Z) by A4, XXREAL_0:1; ::_thesis: verum end; assume for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) = C . (W \/ Z) ; ::_thesis: A in sigma_Field C then for W, Z being Subset of X st W c= A & Z c= X \ A holds (C . W) + (C . Z) <= C . (W \/ Z) ; hence A in sigma_Field C by Def2; ::_thesis: verum end; theorem Th6: :: MEASURE4:6 for X being set for C being C_Measure of X for W, Z being Subset of X st W in sigma_Field C & Z misses W holds C . (W \/ Z) = (C . W) + (C . Z) proof let X be set ; ::_thesis: for C being C_Measure of X for W, Z being Subset of X st W in sigma_Field C & Z misses W holds C . (W \/ Z) = (C . W) + (C . Z) let C be C_Measure of X; ::_thesis: for W, Z being Subset of X st W in sigma_Field C & Z misses W holds C . (W \/ Z) = (C . W) + (C . Z) let W, Z be Subset of X; ::_thesis: ( W in sigma_Field C & Z misses W implies C . (W \/ Z) = (C . W) + (C . Z) ) assume that A1: W in sigma_Field C and A2: Z misses W ; ::_thesis: C . (W \/ Z) = (C . W) + (C . Z) Z \ W c= X \ W by XBOOLE_1:33; then Z c= X \ W by A2, XBOOLE_1:83; hence C . (W \/ Z) = (C . W) + (C . Z) by A1, Th5; ::_thesis: verum end; theorem Th7: :: MEASURE4:7 for A, X being set for C being C_Measure of X st A in sigma_Field C holds X \ A in sigma_Field C proof let A, X be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C holds X \ A in sigma_Field C let C be C_Measure of X; ::_thesis: ( A in sigma_Field C implies X \ A in sigma_Field C ) assume A1: A in sigma_Field C ; ::_thesis: X \ A in sigma_Field C for W, Z being Subset of X st W c= X \ A & Z c= X \ (X \ A) holds (C . W) + (C . Z) <= C . (W \/ Z) proof let W, Z be Subset of X; ::_thesis: ( W c= X \ A & Z c= X \ (X \ A) implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A2: W c= X \ A and A3: Z c= X \ (X \ A) ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) X \ (X \ A) = X /\ A by XBOOLE_1:48; then Z c= A by A1, A3, XBOOLE_1:28; hence (C . W) + (C . Z) <= C . (W \/ Z) by A1, A2, Def2; ::_thesis: verum end; hence X \ A in sigma_Field C by Def2; ::_thesis: verum end; theorem Th8: :: MEASURE4:8 for X, A, B being set for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A \/ B in sigma_Field C proof let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A \/ B in sigma_Field C let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A \/ B in sigma_Field C ) assume that A1: A in sigma_Field C and A2: B in sigma_Field C ; ::_thesis: A \/ B in sigma_Field C reconsider A = A, B = B as Subset of X by A1, A2; set D = A \/ B; for W, Z being Subset of X st W c= A \/ B & Z c= X \ (A \/ B) holds (C . W) + (C . Z) = C . (W \/ Z) proof let W, Z be Subset of X; ::_thesis: ( W c= A \/ B & Z c= X \ (A \/ B) implies (C . W) + (C . Z) = C . (W \/ Z) ) assume that A3: W c= A \/ B and A4: Z c= X \ (A \/ B) ; ::_thesis: (C . W) + (C . Z) = C . (W \/ Z) set W2 = W \ A; set Z1 = (W \ A) \/ Z; A5: (X \ A) /\ (X \ B) c= X \ B by XBOOLE_1:17; set W1 = W /\ A; A6: W /\ A c= A by XBOOLE_1:17; (X \ A) /\ (X \ B) c= X \ A by XBOOLE_1:17; then A7: X \ (A \/ B) c= X \ A by XBOOLE_1:53; Z c= (X \ A) /\ (X \ B) by A4, XBOOLE_1:53; then A8: Z c= X \ B by A5, XBOOLE_1:1; W = (W /\ A) \/ (W \ A) by XBOOLE_1:51; then C . W <= (C . (W /\ A)) + (C . (W \ A)) by Th4; then A9: (C . W) + (C . Z) <= ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) by XXREAL_3:36; W \ A c= (B \/ A) \ A by A3, XBOOLE_1:33; then A10: W \ A c= B \ A by XBOOLE_1:40; B \ A c= B by XBOOLE_1:36; then W \ A c= B by A10, XBOOLE_1:1; then A11: (C . (W \ A)) + (C . Z) <= C . ((W \ A) \/ Z) by A2, A8, Def2; C is V87() by Def1; then A12: 0. <= C . (W /\ A) by MEASURE1:def_2; W \ A c= X \ A by XBOOLE_1:33; then (W \ A) \/ Z c= (X \ A) \/ Z by XBOOLE_1:9; then A13: (W \ A) \/ Z c= X \ A by A4, A7, XBOOLE_1:1, XBOOLE_1:12; C . (W \/ Z) = C . (((W /\ A) \/ (W \ A)) \/ Z) by XBOOLE_1:51 .= C . ((W /\ A) \/ ((W \ A) \/ Z)) by XBOOLE_1:4 .= (C . (W /\ A)) + (C . ((W \ A) \/ Z)) by A1, A6, A13, Th5 ; then A14: (C . (W /\ A)) + ((C . (W \ A)) + (C . Z)) <= C . (W \/ Z) by A11, XXREAL_3:36; A15: C is V87() by Def1; then A16: 0. <= C . Z by MEASURE1:def_2; 0. <= C . (W \ A) by A15, MEASURE1:def_2; then ((C . (W /\ A)) + (C . (W \ A))) + (C . Z) <= C . (W \/ Z) by A16, A12, A14, XXREAL_3:44; then A17: (C . W) + (C . Z) <= C . (W \/ Z) by A9, XXREAL_0:2; C . (W \/ Z) <= (C . W) + (C . Z) by Th4; hence (C . W) + (C . Z) = C . (W \/ Z) by A17, XXREAL_0:1; ::_thesis: verum end; hence A \/ B in sigma_Field C by Th5; ::_thesis: verum end; theorem Th9: :: MEASURE4:9 for X, A, B being set for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A /\ B in sigma_Field C proof let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A /\ B in sigma_Field C let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A /\ B in sigma_Field C ) assume that A1: A in sigma_Field C and A2: B in sigma_Field C ; ::_thesis: A /\ B in sigma_Field C A3: X \ B in sigma_Field C by A2, Th7; A /\ B c= X /\ X by A1, A2, XBOOLE_1:27; then A4: A /\ B = X /\ (A /\ B) by XBOOLE_1:28 .= X \ (X \ (A /\ B)) by XBOOLE_1:48 .= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54 ; X \ A in sigma_Field C by A1, Th7; then (X \ A) \/ (X \ B) in sigma_Field C by A3, Th8; hence A /\ B in sigma_Field C by A4, Th7; ::_thesis: verum end; theorem Th10: :: MEASURE4:10 for X, A, B being set for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A \ B in sigma_Field C proof let X, A, B be set ; ::_thesis: for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds A \ B in sigma_Field C let C be C_Measure of X; ::_thesis: ( A in sigma_Field C & B in sigma_Field C implies A \ B in sigma_Field C ) assume that A1: A in sigma_Field C and A2: B in sigma_Field C ; ::_thesis: A \ B in sigma_Field C for x being set holds ( x in A \ B iff x in A /\ (X \ B) ) proof let x be set ; ::_thesis: ( x in A \ B iff x in A /\ (X \ B) ) hereby ::_thesis: ( x in A /\ (X \ B) implies x in A \ B ) assume A3: x in A \ B ; ::_thesis: x in A /\ (X \ B) then A4: not x in B by XBOOLE_0:def_5; x in A by A3; then x in X \ B by A1, A4, XBOOLE_0:def_5; hence x in A /\ (X \ B) by A3, XBOOLE_0:def_4; ::_thesis: verum end; assume A5: x in A /\ (X \ B) ; ::_thesis: x in A \ B then x in X \ B by XBOOLE_0:def_4; then A6: not x in B by XBOOLE_0:def_5; x in A by A5, XBOOLE_0:def_4; hence x in A \ B by A6, XBOOLE_0:def_5; ::_thesis: verum end; then A7: A \ B = A /\ (X \ B) by TARSKI:1; X \ B in sigma_Field C by A2, Th7; hence A \ B in sigma_Field C by A1, A7, Th9; ::_thesis: verum end; theorem Th11: :: MEASURE4:11 for X being set for S being SigmaField of X for N being Function of NAT,S for A being Element of S ex F being Function of NAT,S st for n being Element of NAT holds F . n = A /\ (N . n) proof let X be set ; ::_thesis: for S being SigmaField of X for N being Function of NAT,S for A being Element of S ex F being Function of NAT,S st for n being Element of NAT holds F . n = A /\ (N . n) let S be SigmaField of X; ::_thesis: for N being Function of NAT,S for A being Element of S ex F being Function of NAT,S st for n being Element of NAT holds F . n = A /\ (N . n) let N be Function of NAT,S; ::_thesis: for A being Element of S ex F being Function of NAT,S st for n being Element of NAT holds F . n = A /\ (N . n) let A be Element of S; ::_thesis: ex F being Function of NAT,S st for n being Element of NAT holds F . n = A /\ (N . n) defpred S1[ set , set ] means ( \$1 in NAT implies \$2 = A /\ (N . \$1) ); A1: for x being set st x in NAT holds ex y being set st ( y in S & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in S & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in S & S1[x,y] ) then reconsider x = x as Element of NAT ; consider y being set such that A2: y = A /\ (N . x) ; take y ; ::_thesis: ( y in S & S1[x,y] ) thus ( y in S & S1[x,y] ) by A2; ::_thesis: verum end; ex F being Function of NAT,S st for x being set st x in NAT holds S1[x,F . x] from FUNCT_2:sch_1(A1); then consider F being Function of NAT,S such that A3: for x being set st x in NAT holds S1[x,F . x] ; take F ; ::_thesis: for n being Element of NAT holds F . n = A /\ (N . n) thus for n being Element of NAT holds F . n = A /\ (N . n) by A3; ::_thesis: verum end; theorem Th12: :: MEASURE4:12 for X being set for C being C_Measure of X holds sigma_Field C is SigmaField of X proof let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Field C is SigmaField of X let C be C_Measure of X; ::_thesis: sigma_Field C is SigmaField of X A1: C is V87() by Def1; A2: for M being N_Sub_set_fam of X st M c= sigma_Field C holds union M in sigma_Field C proof let M be N_Sub_set_fam of X; ::_thesis: ( M c= sigma_Field C implies union M in sigma_Field C ) assume A3: M c= sigma_Field C ; ::_thesis: union M in sigma_Field C for W, Z being Subset of X st W c= union M & Z c= X \ (union M) holds (C . W) + (C . Z) <= C . (W \/ Z) proof reconsider S = bool X as SigmaField of X by Th3; let W, Z be Subset of X; ::_thesis: ( W c= union M & Z c= X \ (union M) implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A4: W c= union M and A5: Z c= X \ (union M) ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) consider F being Function of NAT,(bool X) such that A6: rng F = M by SUPINF_2:def_8; consider G being Function of NAT,S such that A7: G . 0 = F . 0 and A8: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4; consider B being Function of NAT,S such that A9: B . 0 = F . 0 and A10: for n being Element of NAT holds B . (n + 1) = (F . (n + 1)) \ (G . n) by MEASURE2:8; A11: union (rng F) = union (rng B) by A7, A8, A9, A10, Th2; defpred S1[ Element of NAT ] means G . \$1 in sigma_Field C; A12: for n being Element of NAT holds F . n in sigma_Field C proof let n be Element of NAT ; ::_thesis: F . n in sigma_Field C F . n in M by A6, FUNCT_2:4; hence F . n in sigma_Field C by A3; ::_thesis: verum end; A13: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A14: G . k in sigma_Field C ; ::_thesis: S1[k + 1] A15: F . (k + 1) in sigma_Field C by A12; G . (k + 1) = (F . (k + 1)) \/ (G . k) by A8; hence S1[k + 1] by A14, A15, Th8; ::_thesis: verum end; A16: S1[ 0 ] by A12, A7; A17: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A13); consider Q being Function of NAT,S such that A18: for n being Element of NAT holds Q . n = W /\ (B . n) by Th11; A19: union (rng Q) = W /\ (union (rng B)) by A18, Th1; consider QQ being Function of NAT,S such that A20: QQ . 0 = Q . 0 and A21: for n being Element of NAT holds QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by MEASURE2:4; reconsider Q = Q, QQ = QQ, F = F, G = G as Function of NAT,(bool X) ; A22: F . 0 in sigma_Field C by A12; defpred S2[ Element of NAT ] means C . (Z \/ (QQ . \$1)) = (C . Z) + ((Ser (C * Q)) . \$1); A23: C * Q is V87() by A1, MEASURE1:25; A24: for k being Element of NAT st S2[k] holds S2[k + 1] proof defpred S3[ Element of NAT ] means QQ . \$1 c= G . \$1; let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) A25: (F . (k + 1)) \ (G . k) c= F . (k + 1) by XBOOLE_1:36; A26: QQ . (k + 1) = (QQ . k) \/ (Q . (k + 1)) by A21; A27: G . k in sigma_Field C by A17; F . (k + 1) in sigma_Field C by A12; then A28: (F . (k + 1)) \ (G . k) in sigma_Field C by A27, Th10; A29: 0. <= (C * Q) . (k + 1) by A23, SUPINF_2:39; A30: 0. <= (Ser (C * Q)) . k by A23, SUPINF_2:40; QQ . 0 = W /\ (F . 0) by A9, A18, A20; then A31: S3[ 0 ] by A7, XBOOLE_1:17; for n being Element of NAT holds QQ . n misses (F . (n + 1)) \ (G . n) proof let n be Element of NAT ; ::_thesis: QQ . n misses (F . (n + 1)) \ (G . n) A32: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume A33: QQ . n c= G . n ; ::_thesis: S3[n + 1] A34: W /\ (F . (n + 1)) c= F . (n + 1) by XBOOLE_1:17; W /\ ((F . (n + 1)) \ (G . n)) c= W /\ (F . (n + 1)) by XBOOLE_1:26, XBOOLE_1:36; then A35: W /\ ((F . (n + 1)) \ (G . n)) c= F . (n + 1) by A34, XBOOLE_1:1; QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by A21 .= (W /\ (B . (n + 1))) \/ (QQ . n) by A18 .= (W /\ ((F . (n + 1)) \ (G . n))) \/ (QQ . n) by A10 ; then QQ . (n + 1) c= (F . (n + 1)) \/ (G . n) by A33, A35, XBOOLE_1:13; hence S3[n + 1] by A8; ::_thesis: verum end; A36: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A31, A32); G . n misses (F . (n + 1)) \ (G . n) by XBOOLE_1:79; hence QQ . n misses (F . (n + 1)) \ (G . n) by A36, XBOOLE_1:63; ::_thesis: verum end; then QQ . k misses (F . (k + 1)) \ (G . k) ; then A37: (QQ . k) /\ ((F . (k + 1)) \ (G . k)) = {} by XBOOLE_0:def_7; A38: QQ . k c= X \ ((F . (k + 1)) \ (G . k)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in QQ . k or z in X \ ((F . (k + 1)) \ (G . k)) ) assume A39: z in QQ . k ; ::_thesis: z in X \ ((F . (k + 1)) \ (G . k)) then not z in (F . (k + 1)) \ (G . k) by A37, XBOOLE_0:def_4; hence z in X \ ((F . (k + 1)) \ (G . k)) by A39, XBOOLE_0:def_5; ::_thesis: verum end; Q . (k + 1) = W /\ (B . (k + 1)) by A18 .= W /\ ((F . (k + 1)) \ (G . k)) by A10 ; then A40: Q . (k + 1) c= (F . (k + 1)) \ (G . k) by XBOOLE_1:17; F . (k + 1) c= union (rng F) by FUNCT_2:4, ZFMISC_1:74; then (F . (k + 1)) \ (G . k) c= union (rng F) by A25, XBOOLE_1:1; then X \ (union (rng F)) c= X \ ((F . (k + 1)) \ (G . k)) by XBOOLE_1:34; then Z c= X \ ((F . (k + 1)) \ (G . k)) by A5, A6, XBOOLE_1:1; then Z \/ (QQ . k) c= X \ ((F . (k + 1)) \ (G . k)) by A38, XBOOLE_1:8; then A41: (C . (Q . (k + 1))) + (C . (Z \/ (QQ . k))) = C . ((Z \/ (QQ . k)) \/ (Q . (k + 1))) by A40, A28, Th5 .= C . (Z \/ (QQ . (k + 1))) by A26, XBOOLE_1:4 ; A42: 0. <= C . Z by A1, SUPINF_2:39; assume C . (Z \/ (QQ . k)) = (C . Z) + ((Ser (C * Q)) . k) ; ::_thesis: S2[k + 1] then C . (Z \/ (QQ . (k + 1))) = ((C . Z) + ((Ser (C * Q)) . k)) + ((C * Q) . (k + 1)) by A41, FUNCT_2:15 .= (C . Z) + (((Ser (C * Q)) . k) + ((C * Q) . (k + 1))) by A42, A30, A29, XXREAL_3:44 .= (C . Z) + ((Ser (C * Q)) . (k + 1)) by SUPINF_2:44 ; hence S2[k + 1] ; ::_thesis: verum end; QQ . 0 = W /\ (F . 0) by A9, A18, A20; then A43: QQ . 0 c= F . 0 by XBOOLE_1:17; A44: (Ser (C * Q)) . 0 = (C * Q) . 0 by SUPINF_2:44 .= C . (QQ . 0) by A20, FUNCT_2:15 ; F . 0 in rng F by FUNCT_2:4; then X \ (union (rng F)) c= X \ (F . 0) by XBOOLE_1:34, ZFMISC_1:74; then Z c= X \ (F . 0) by A5, A6, XBOOLE_1:1; then A45: S2[ 0 ] by A22, A43, A44, Th5; A46: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A45, A24); defpred S3[ Element of NAT ] means QQ . \$1 c= W; A47: for n being Element of NAT st S3[n] holds S3[n + 1] proof let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] ) assume A48: QQ . n c= W ; ::_thesis: S3[n + 1] A49: W /\ (B . (n + 1)) c= W by XBOOLE_1:17; QQ . (n + 1) = (Q . (n + 1)) \/ (QQ . n) by A21 .= (W /\ (B . (n + 1))) \/ (QQ . n) by A18 ; then QQ . (n + 1) c= W \/ W by A48, A49, XBOOLE_1:13; hence S3[n + 1] ; ::_thesis: verum end; QQ . 0 = W /\ (B . 0) by A18, A20; then A50: S3[ 0 ] by XBOOLE_1:17; A51: for n being Element of NAT holds S3[n] from NAT_1:sch_1(A50, A47); A52: union (rng Q) = W by A4, A6, A11, A19, XBOOLE_1:28; A53: ( C . Z is real implies (C . W) + (C . Z) <= C . (W \/ Z) ) proof defpred S4[ set , set ] means ( ( \$1 = 0 implies \$2 = (C . (Z \/ W)) - (C . Z) ) & ( \$1 <> 0 implies \$2 = 0. ) ); A54: for x being set st x in NAT holds ex y being set st ( y in ExtREAL & S4[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in ExtREAL & S4[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in ExtREAL & S4[x,y] ) then reconsider x = x as Element of NAT ; ( x <> 0 implies ex y being set st ( y in ExtREAL & S4[x,y] ) ) ; hence ex y being set st ( y in ExtREAL & S4[x,y] ) ; ::_thesis: verum end; consider R being Function of NAT,ExtREAL such that A55: for x being set st x in NAT holds S4[x,R . x] from FUNCT_2:sch_1(A54); assume A56: C . Z is real ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) for n being Element of NAT holds 0. <= R . n proof let n be Element of NAT ; ::_thesis: 0. <= R . n ( C . Z in REAL or C . Z in {-infty,+infty} ) by XBOOLE_0:def_3, XXREAL_0:def_4; then consider y being Real such that A57: y = C . Z by A56, TARSKI:def_2; Z c= Z \/ W by XBOOLE_1:7; then C . Z <= C . (Z \/ W) by Def1; then A58: (C . Z) - (C . Z) <= (C . (Z \/ W)) - (C . Z) by XXREAL_3:37; (C . Z) - (C . Z) = y - y by A57, SUPINF_2:3; hence 0. <= R . n by A55, A58; ::_thesis: verum end; then A59: R is V87() by SUPINF_2:39; A60: for n being Element of NAT holds (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z) proof let n be Element of NAT ; ::_thesis: (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z) A61: Z \/ (QQ . n) c= Z \/ W by A51, XBOOLE_1:9; ((Ser (C * Q)) . n) + (C . Z) = C . (Z \/ (QQ . n)) by A46; then ((Ser (C * Q)) . n) + (C . Z) <= C . (Z \/ W) by A61, Def1; hence (Ser (C * Q)) . n <= (C . (Z \/ W)) - (C . Z) by A56, XXREAL_3:45; ::_thesis: verum end; A62: for n being Element of NAT holds (Ser (C * Q)) . n <= (Ser R) . n proof let n be Element of NAT ; ::_thesis: (Ser (C * Q)) . n <= (Ser R) . n defpred S5[ Element of NAT ] means (Ser R) . \$1 = (C . (Z \/ W)) - (C . Z); A63: for k being Element of NAT st S5[k] holds S5[k + 1] proof let k be Element of NAT ; ::_thesis: ( S5[k] implies S5[k + 1] ) assume A64: (Ser R) . k = (C . (Z \/ W)) - (C . Z) ; ::_thesis: S5[k + 1] set y = (Ser R) . k; thus (Ser R) . (k + 1) = ((Ser R) . k) + (R . (k + 1)) by SUPINF_2:44 .= ((Ser R) . k) + 0. by A55 .= (C . (Z \/ W)) - (C . Z) by A64, XXREAL_3:4 ; ::_thesis: verum end; (Ser R) . 0 = R . 0 by SUPINF_2:44; then A65: S5[ 0 ] by A55; for k being Element of NAT holds S5[k] from NAT_1:sch_1(A65, A63); then (Ser R) . n = (C . (Z \/ W)) - (C . Z) ; hence (Ser (C * Q)) . n <= (Ser R) . n by A60; ::_thesis: verum end; set y = (Ser R) . 0; (Ser R) . 0 = R . 0 by SUPINF_2:44; then A66: (Ser R) . 0 = (C . (Z \/ W)) - (C . Z) by A55; A67: C . W <= SUM (C * Q) by A52, Def1; for k being Element of NAT st 1 <= k holds R . k = 0. by A55; then A68: SUM R = (Ser R) . 1 by A59, SUPINF_2:48; (Ser R) . 1 = ((Ser R) . 0) + (R . (0 + 1)) by SUPINF_2:44 .= ((Ser R) . 0) + 0. by A55 .= (C . (Z \/ W)) - (C . Z) by A66, XXREAL_3:4 ; then SUM (C * Q) <= (C . (Z \/ W)) - (C . Z) by A62, A68, MEASURE3:1; then C . W <= (C . (Z \/ W)) - (C . Z) by A67, XXREAL_0:2; hence (C . W) + (C . Z) <= C . (W \/ Z) by A56, XXREAL_3:45; ::_thesis: verum end; A69: ( C . Z = +infty implies (C . W) + (C . Z) <= C . (W \/ Z) ) proof A70: Z c= W \/ Z by XBOOLE_1:7; assume A71: C . Z = +infty ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) 0. <= C . W by A1, MEASURE1:def_2; then (C . W) + (C . Z) = +infty by A71, XXREAL_3:def_2; hence (C . W) + (C . Z) <= C . (W \/ Z) by A71, A70, Def1; ::_thesis: verum end; 0 <= C . Z by A1, MEASURE1:def_2; then ( C . Z is Element of REAL or C . Z = +infty ) by XXREAL_0:14; hence (C . W) + (C . Z) <= C . (W \/ Z) by A69, A53; ::_thesis: verum end; hence union M in sigma_Field C by Def2; ::_thesis: verum end; for A being set st A in sigma_Field C holds X \ A in sigma_Field C by Th7; then reconsider Y = sigma_Field C as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def_1, MEASURE1:def_5; Y is SigmaField of X ; hence sigma_Field C is SigmaField of X ; ::_thesis: verum end; registration let X be set ; let C be C_Measure of X; cluster sigma_Field C -> non empty compl-closed sigma-additive ; coherence ( sigma_Field C is sigma-additive & sigma_Field C is compl-closed & not sigma_Field C is empty ) by Th12; end; definition let X be set ; let S be SigmaField of X; let A be N_Sub_fam of S; :: original: union redefine func union A -> Element of S; coherence union A is Element of S proof A c= S by MEASURE2:def_1; hence union A is Element of S by MEASURE1:def_5; ::_thesis: verum end; end; definition let X be set ; let C be C_Measure of X; func sigma_Meas C -> Function of (sigma_Field C),ExtREAL means :Def3: :: MEASURE4:def 3 for A being Subset of X st A in sigma_Field C holds it . A = C . A; existence ex b1 being Function of (sigma_Field C),ExtREAL st for A being Subset of X st A in sigma_Field C holds b1 . A = C . A proof ex D being Function of (sigma_Field C),ExtREAL st for A being Subset of X st A in sigma_Field C holds D . A = C . A proof deffunc H1( set ) -> Element of ExtREAL = C . \$1; A1: for S being set st S in sigma_Field C holds H1(S) in ExtREAL ; consider D being Function of (sigma_Field C),ExtREAL such that A2: for S being set st S in sigma_Field C holds D . S = H1(S) from FUNCT_2:sch_2(A1); take D ; ::_thesis: for A being Subset of X st A in sigma_Field C holds D . A = C . A thus for A being Subset of X st A in sigma_Field C holds D . A = C . A by A2; ::_thesis: verum end; then consider D being Function of (sigma_Field C),ExtREAL such that A3: for A being Subset of X st A in sigma_Field C holds D . A = C . A ; take D ; ::_thesis: for A being Subset of X st A in sigma_Field C holds D . A = C . A thus for A being Subset of X st A in sigma_Field C holds D . A = C . A by A3; ::_thesis: verum end; uniqueness for b1, b2 being Function of (sigma_Field C),ExtREAL st ( for A being Subset of X st A in sigma_Field C holds b1 . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds b2 . A = C . A ) holds b1 = b2 proof let D1, D2 be Function of (sigma_Field C),ExtREAL; ::_thesis: ( ( for A being Subset of X st A in sigma_Field C holds D1 . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds D2 . A = C . A ) implies D1 = D2 ) assume that A4: for A being Subset of X st A in sigma_Field C holds D1 . A = C . A and A5: for A being Subset of X st A in sigma_Field C holds D2 . A = C . A ; ::_thesis: D1 = D2 A6: for A being set st A in sigma_Field C holds D1 . A = D2 . A proof let A be set ; ::_thesis: ( A in sigma_Field C implies D1 . A = D2 . A ) assume A7: A in sigma_Field C ; ::_thesis: D1 . A = D2 . A then reconsider A = A as Subset of X ; D1 . A = C . A by A4, A7 .= D2 . A by A5, A7 ; hence D1 . A = D2 . A ; ::_thesis: verum end; A8: sigma_Field C = dom D2 by FUNCT_2:def_1; sigma_Field C = dom D1 by FUNCT_2:def_1; hence D1 = D2 by A8, A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines sigma_Meas MEASURE4:def_3_:_ for X being set for C being C_Measure of X for b3 being Function of (sigma_Field C),ExtREAL holds ( b3 = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds b3 . A = C . A ); theorem Th13: :: MEASURE4:13 for X being set for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C) proof let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C) let C be C_Measure of X; ::_thesis: sigma_Meas C is Measure of (sigma_Field C) A1: now__::_thesis:_for_A_being_Element_of_sigma_Field_C_holds_0._<=_(sigma_Meas_C)_._A let A be Element of sigma_Field C; ::_thesis: 0. <= (sigma_Meas C) . A reconsider A9 = A as Subset of X ; A2: C is V87() by Def1; (sigma_Meas C) . A9 = C . A9 by Def3; hence 0. <= (sigma_Meas C) . A by A2, MEASURE1:def_2; ::_thesis: verum end; {} in sigma_Field C by PROB_1:4; then A3: (sigma_Meas C) . {} = C . {} by Def3; A4: now__::_thesis:_for_A,_B_being_Element_of_sigma_Field_C_st_A_misses_B_holds_ (sigma_Meas_C)_._(A_\/_B)_=_((sigma_Meas_C)_._A)_+_((sigma_Meas_C)_._B) let A, B be Element of sigma_Field C; ::_thesis: ( A misses B implies (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) ) reconsider A9 = A, B9 = B as Subset of X ; A5: (sigma_Meas C) . B9 = C . B9 by Def3; assume A misses B ; ::_thesis: (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) then A6: C . (A9 \/ B9) = (C . A9) + (C . B9) by Th6; (sigma_Meas C) . A9 = C . A9 by Def3; hence (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) by A5, A6, Def3; ::_thesis: verum end; C is zeroed by Def1; then (sigma_Meas C) . {} = 0. by A3, VALUED_0:def_19; hence sigma_Meas C is Measure of (sigma_Field C) by A1, A4, MEASURE1:def_2, MEASURE1:def_3, VALUED_0:def_19; ::_thesis: verum end; theorem Th14: :: MEASURE4:14 for X being set for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C) proof let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C) let C be C_Measure of X; ::_thesis: sigma_Meas C is sigma_Measure of (sigma_Field C) reconsider M = sigma_Meas C as Measure of (sigma_Field C) by Th13; for F being Sep_Sequence of (sigma_Field C) holds M . (union (rng F)) <= SUM (M * F) proof let F be Sep_Sequence of (sigma_Field C); ::_thesis: M . (union (rng F)) <= SUM (M * F) consider A being Subset of X such that A1: A = union (rng F) ; A2: for k being set st k in NAT holds (M * F) . k = (C * F) . k proof let k be set ; ::_thesis: ( k in NAT implies (M * F) . k = (C * F) . k ) assume A3: k in NAT ; ::_thesis: (M * F) . k = (C * F) . k then A4: (M * F) . k = M . (F . k) by FUNCT_2:15; A5: F . k in sigma_Field C by A3, FUNCT_2:5; reconsider F = F as Function of NAT,(bool X) by FUNCT_2:7; (C * F) . k = C . (F . k) by A3, FUNCT_2:15; hence (M * F) . k = (C * F) . k by A4, A5, Def3; ::_thesis: verum end; reconsider F9 = F as Function of NAT,(bool X) by FUNCT_2:7; consider a, b being R_eal such that a = M . A and A6: b = C . A ; C * F9 is Function of NAT,ExtREAL ; then A7: M * F = C * F by A2, FUNCT_2:12; reconsider F = F as Function of NAT,(bool X) by FUNCT_2:7; b <= SUM (C * F) by A1, A6, Def1; hence M . (union (rng F)) <= SUM (M * F) by A1, A6, A7, Def3; ::_thesis: verum end; hence sigma_Meas C is sigma_Measure of (sigma_Field C) by MEASURE3:14; ::_thesis: verum end; registration let X be set ; let C be C_Measure of X; cluster sigma_Meas C -> zeroed V87() sigma-additive ; coherence ( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th14; end; theorem Th15: :: MEASURE4:15 for X being set for C being C_Measure of X for A being Subset of X st C . A = 0. holds A in sigma_Field C proof let X be set ; ::_thesis: for C being C_Measure of X for A being Subset of X st C . A = 0. holds A in sigma_Field C let C be C_Measure of X; ::_thesis: for A being Subset of X st C . A = 0. holds A in sigma_Field C let A be Subset of X; ::_thesis: ( C . A = 0. implies A in sigma_Field C ) assume A1: C . A = 0. ; ::_thesis: A in sigma_Field C now__::_thesis:_for_W,_Z_being_Subset_of_X_st_W_c=_A_&_Z_c=_X_\_A_holds_ (C_._W)_+_(C_._Z)_<=_C_._(W_\/_Z) let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) ) assume that A2: W c= A and Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z) Z c= W \/ Z by XBOOLE_1:7; then A3: C . Z <= C . (W \/ Z) by Def1; C is V87() by Def1; then 0. <= C . W by MEASURE1:def_2; then C . W = 0. by A1, A2, Def1; hence (C . W) + (C . Z) <= C . (W \/ Z) by A3, XXREAL_3:4; ::_thesis: verum end; hence A in sigma_Field C by Def2; ::_thesis: verum end; theorem :: MEASURE4:16 for X being set for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C proof let X be set ; ::_thesis: for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C let C be C_Measure of X; ::_thesis: sigma_Meas C is_complete sigma_Field C let A be Subset of X; :: according to MEASURE3:def_1 ::_thesis: for b1 being set holds ( not b1 in sigma_Field C or not A c= b1 or not (sigma_Meas C) . b1 = 0. or A in sigma_Field C ) let B be set ; ::_thesis: ( not B in sigma_Field C or not A c= B or not (sigma_Meas C) . B = 0. or A in sigma_Field C ) assume that A1: B in sigma_Field C and A2: A c= B and A3: (sigma_Meas C) . B = 0. ; ::_thesis: A in sigma_Field C reconsider B = B as Subset of X by A1; C is V87() by Def1; then A4: 0. <= C . A by MEASURE1:def_2; C . B = 0. by A1, A3, Def3; then C . A = 0. by A2, A4, Def1; hence A in sigma_Field C by Th15; ::_thesis: verum end;