let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let M be Measure of F; :: thesis: for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let Sets be SetSequence of X; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let F be Field_Subset of X; :: thesis: for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let M be Measure of F; :: thesis: for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

let Sets be SetSequence of X; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

A1: now :: thesis: ( ( for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty} ) implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

assume A2:
for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty}
; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets)))

end;inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets)))

proof

hence
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
by Def8; :: thesis: verum
set y = inf (Svc (M,(union (rng Sets))));

set x = sup (rng (Ser ((C_Meas M) * Sets)));

A3: (Ser ((C_Meas M) * Sets)) . 0 <= sup (rng (Ser ((C_Meas M) * Sets))) by FUNCT_2:4, XXREAL_2:4;

A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;

then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:39;

then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:def 11;

assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; :: thesis: contradiction

then consider eps being Real such that

A6: 0 < eps and

A7: (sup (rng (Ser ((C_Meas M) * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by A5, A3, XXREAL_3:49;

consider E being sequence of ExtREAL such that

A8: for n being Nat holds 0 < E . n and

A9: SUM E < eps by A6, MEASURE6:4;

for n being Element of NAT holds 0 <= E . n by A8;

then A10: E is nonnegative by SUPINF_2:39;

defpred S_{1}[ Element of NAT , set ] means ex F0 being Covering of Sets . $1,F st

( $2 = F0 & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . $1)))) + (E . $1) );

A11: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool X)) st S_{1}[n,F0]

A18: for n being Element of NAT holds S_{1}[n,FF . n]
from FUNCT_2:sch 3(A11);

A19: for n being Nat holds FF . n is Covering of Sets . n,F_{1}( Element of NAT ) -> object = (((C_Meas M) * Sets) . $1) + (E . $1);

A20: for x being Element of NAT holds H_{1}(x) is Element of ExtREAL
by XXREAL_0:def 1;

consider G0 being sequence of ExtREAL such that

A21: for n being Element of NAT holds G0 . n = H_{1}(n)
from FUNCT_2:sch 9(A20);

reconsider FF = FF as Covering of Sets,F by A19, Def4;

for n being Element of NAT holds (Volume (M,FF)) . n <= G0 . n

then SUM G0 <= (SUM ((C_Meas M) * Sets)) + eps by A4, A10, A23, Th3;

then A24: SUM (Volume (M,FF)) <= (SUM ((C_Meas M) * Sets)) + eps by A22, XXREAL_0:2;

inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,FF)) by Th7;

hence contradiction by A7, A24, XXREAL_0:2; :: thesis: verum

end;set x = sup (rng (Ser ((C_Meas M) * Sets)));

A3: (Ser ((C_Meas M) * Sets)) . 0 <= sup (rng (Ser ((C_Meas M) * Sets))) by FUNCT_2:4, XXREAL_2:4;

A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;

then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:39;

then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:def 11;

assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; :: thesis: contradiction

then consider eps being Real such that

A6: 0 < eps and

A7: (sup (rng (Ser ((C_Meas M) * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by A5, A3, XXREAL_3:49;

consider E being sequence of ExtREAL such that

A8: for n being Nat holds 0 < E . n and

A9: SUM E < eps by A6, MEASURE6:4;

for n being Element of NAT holds 0 <= E . n by A8;

then A10: E is nonnegative by SUPINF_2:39;

defpred S

( $2 = F0 & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . $1)))) + (E . $1) );

A11: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool X)) st S

proof

consider FF being sequence of (Funcs (NAT,(bool X))) such that
let n be Element of NAT ; :: thesis: ex F0 being Element of Funcs (NAT,(bool X)) st S_{1}[n,F0]

( C_Meas M is nonnegative & (C_Meas M) . (Sets . n) = inf (Svc (M,(Sets . n))) ) by Def8, Th10;

then A12: ( 0 in REAL & 0. <= inf (Svc (M,(Sets . n))) ) by SUPINF_2:51, XREAL_0:def 1;

Svc (M,(Sets . n)) <> {+infty} by A2;

then not Svc (M,(Sets . n)) c= {+infty} by ZFMISC_1:33;

then (Svc (M,(Sets . n))) \ {+infty} <> {} by XBOOLE_1:37;

then consider x being object such that

A13: x in (Svc (M,(Sets . n))) \ {+infty} by XBOOLE_0:def 1;

reconsider x = x as R_eal by A13;

not x in {+infty} by A13, XBOOLE_0:def 5;

then A14: x <> +infty by TARSKI:def 1;

x in Svc (M,(Sets . n)) by A13, XBOOLE_0:def 5;

then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3;

then inf (Svc (M,(Sets . n))) < +infty by A14, XXREAL_0:2, XXREAL_0:4;

then inf (Svc (M,(Sets . n))) is Element of REAL by A12, XXREAL_0:46;

then consider S1 being ExtReal such that

A15: S1 in Svc (M,(Sets . n)) and

A16: S1 < (inf (Svc (M,(Sets . n)))) + (E . n) by A8, MEASURE6:5;

consider FS being Covering of Sets . n,F such that

A17: S1 = SUM (vol (M,FS)) by A15, Def7;

reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;

take FS ; :: thesis: S_{1}[n,FS]

thus S_{1}[n,FS]
by A16, A17; :: thesis: verum

end;( C_Meas M is nonnegative & (C_Meas M) . (Sets . n) = inf (Svc (M,(Sets . n))) ) by Def8, Th10;

then A12: ( 0 in REAL & 0. <= inf (Svc (M,(Sets . n))) ) by SUPINF_2:51, XREAL_0:def 1;

Svc (M,(Sets . n)) <> {+infty} by A2;

then not Svc (M,(Sets . n)) c= {+infty} by ZFMISC_1:33;

then (Svc (M,(Sets . n))) \ {+infty} <> {} by XBOOLE_1:37;

then consider x being object such that

A13: x in (Svc (M,(Sets . n))) \ {+infty} by XBOOLE_0:def 1;

reconsider x = x as R_eal by A13;

not x in {+infty} by A13, XBOOLE_0:def 5;

then A14: x <> +infty by TARSKI:def 1;

x in Svc (M,(Sets . n)) by A13, XBOOLE_0:def 5;

then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3;

then inf (Svc (M,(Sets . n))) < +infty by A14, XXREAL_0:2, XXREAL_0:4;

then inf (Svc (M,(Sets . n))) is Element of REAL by A12, XXREAL_0:46;

then consider S1 being ExtReal such that

A15: S1 in Svc (M,(Sets . n)) and

A16: S1 < (inf (Svc (M,(Sets . n)))) + (E . n) by A8, MEASURE6:5;

consider FS being Covering of Sets . n,F such that

A17: S1 = SUM (vol (M,FS)) by A15, Def7;

reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;

take FS ; :: thesis: S

thus S

A18: for n being Element of NAT holds S

A19: for n being Nat holds FF . n is Covering of Sets . n,F

proof

deffunc H
let n be Nat; :: thesis: FF . n is Covering of Sets . n,F

n in NAT by ORDINAL1:def 12;

then ex F0 being Covering of Sets . n,F st

( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) by A18;

hence FF . n is Covering of Sets . n,F ; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then ex F0 being Covering of Sets . n,F st

( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) by A18;

hence FF . n is Covering of Sets . n,F ; :: thesis: verum

A20: for x being Element of NAT holds H

consider G0 being sequence of ExtREAL such that

A21: for n being Element of NAT holds G0 . n = H

reconsider FF = FF as Covering of Sets,F by A19, Def4;

for n being Element of NAT holds (Volume (M,FF)) . n <= G0 . n

proof

then A22:
SUM (Volume (M,FF)) <= SUM G0
by SUPINF_2:43;
let n be Element of NAT ; :: thesis: (Volume (M,FF)) . n <= G0 . n

( ex F0 being Covering of Sets . n,F st

( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) & ((C_Meas M) * Sets) . n = (C_Meas M) . (Sets . n) ) by A18, FUNCT_2:15;

then SUM (vol (M,(FF . n))) < (((C_Meas M) * Sets) . n) + (E . n) by Def8;

then (Volume (M,FF)) . n < (((C_Meas M) * Sets) . n) + (E . n) by Def6;

hence (Volume (M,FF)) . n <= G0 . n by A21; :: thesis: verum

end;( ex F0 being Covering of Sets . n,F st

( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) & ((C_Meas M) * Sets) . n = (C_Meas M) . (Sets . n) ) by A18, FUNCT_2:15;

then SUM (vol (M,(FF . n))) < (((C_Meas M) * Sets) . n) + (E . n) by Def8;

then (Volume (M,FF)) . n < (((C_Meas M) * Sets) . n) + (E . n) by Def6;

hence (Volume (M,FF)) . n <= G0 . n by A21; :: thesis: verum

A23: now :: thesis: for n being Nat holds G0 . n = (((C_Meas M) * Sets) . n) + (E . n)

(SUM ((C_Meas M) * Sets)) + (SUM E) <= (SUM ((C_Meas M) * Sets)) + eps
by A9, XXREAL_3:36;let n be Nat; :: thesis: G0 . n = (((C_Meas M) * Sets) . n) + (E . n)

n is Element of NAT by ORDINAL1:def 12;

hence G0 . n = (((C_Meas M) * Sets) . n) + (E . n) by A21; :: thesis: verum

end;n is Element of NAT by ORDINAL1:def 12;

hence G0 . n = (((C_Meas M) * Sets) . n) + (E . n) by A21; :: thesis: verum

then SUM G0 <= (SUM ((C_Meas M) * Sets)) + eps by A4, A10, A23, Th3;

then A24: SUM (Volume (M,FF)) <= (SUM ((C_Meas M) * Sets)) + eps by A22, XXREAL_0:2;

inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,FF)) by Th7;

hence contradiction by A7, A24, XXREAL_0:2; :: thesis: verum

now :: thesis: ( ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty} implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )

hence
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
by A1; :: thesis: verumassume
ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty}
; :: thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

then consider n being Element of NAT such that

A25: Svc (M,(Sets . n)) = {+infty} ;

inf {+infty} = +infty by XXREAL_2:13;

then (C_Meas M) . (Sets . n) = +infty by A25, Def8;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Lm2; :: thesis: verum

end;then consider n being Element of NAT such that

A25: Svc (M,(Sets . n)) = {+infty} ;

inf {+infty} = +infty by XXREAL_2:13;

then (C_Meas M) . (Sets . n) = +infty by A25, Def8;

hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Lm2; :: thesis: verum