let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
let F be Field_Subset of X; :: thesis: for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
let M be Measure of F; :: thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
let Sets be SetSequence of X; :: thesis: for Cvr being Covering of Sets,F holds inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
let Cvr be Covering of Sets,F; :: thesis: inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
set Q = SUM (vol M,(On Cvr));
for x being ext-real number st x in rng (Ser (vol M,(On Cvr))) holds
ex y being ext-real number st
( y in rng (Ser (Volume M,Cvr)) & x <= y )
proof
let x be
ext-real number ;
:: thesis: ( x in rng (Ser (vol M,(On Cvr))) implies ex y being ext-real number st
( y in rng (Ser (Volume M,Cvr)) & x <= y ) )
assume
x in rng (Ser (vol M,(On Cvr)))
;
:: thesis: ex y being ext-real number st
( y in rng (Ser (Volume M,Cvr)) & x <= y )
then consider n being
Element of
NAT such that A4:
x = (Ser (vol M,(On Cvr))) . n
by FUNCT_2:190;
consider m being
Nat such that A5:
for
Sets being
SetSequence of
X for
G being
Covering of
Sets,
F holds
(Partial_Sums (vol M,(On G))) . n <= (Partial_Sums (Volume M,G)) . m
by Th15x;
B5:
for
Sets being
SetSequence of
X for
G being
Covering of
Sets,
F holds
(Ser (vol M,(On G))) . n <= (Ser (Volume M,G)) . m
proof
let Sets be
SetSequence of
X;
:: thesis: for G being Covering of Sets,F holds (Ser (vol M,(On G))) . n <= (Ser (Volume M,G)) . mlet G be
Covering of
Sets,
F;
:: thesis: (Ser (vol M,(On G))) . n <= (Ser (Volume M,G)) . m
(Partial_Sums (vol M,(On G))) . n <= (Partial_Sums (Volume M,G)) . m
by A5;
then
(Ser (vol M,(On G))) . n <= (Partial_Sums (Volume M,G)) . m
by Lem12;
hence
(Ser (vol M,(On G))) . n <= (Ser (Volume M,G)) . m
by Lem12;
:: thesis: verum
end;
take
(Ser (Volume M,Cvr)) . m
;
:: thesis: ( (Ser (Volume M,Cvr)) . m in rng (Ser (Volume M,Cvr)) & x <= (Ser (Volume M,Cvr)) . m )
m in NAT
by ORDINAL1:def 13;
hence
(
(Ser (Volume M,Cvr)) . m in rng (Ser (Volume M,Cvr)) &
x <= (Ser (Volume M,Cvr)) . m )
by A4, B5, FUNCT_2:6;
:: thesis: verum
end;
then A6:
SUM (vol M,(On Cvr)) <= SUM (Volume M,Cvr)
by XXREAL_2:63;
SUM (vol M,(On Cvr)) in Svc M,(union (rng Sets))
by Def8;
then
inf (Svc M,(union (rng Sets))) <= SUM (vol M,(On Cvr))
by XXREAL_2:3;
hence
inf (Svc M,(union (rng Sets))) <= SUM (Volume M,Cvr)
by A6, XXREAL_0:2; :: thesis: verum