let X be set ; for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let F be Field_Subset of X; for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let M be Measure of F; ( M is completely-additive implies for A being set st A in F holds
M . A = (C_Meas M) . A )
assume A1:
M is completely-additive
; for A being set st A in F holds
M . A = (C_Meas M) . A
let A be set ; ( A in F implies M . A = (C_Meas M) . A )
assume A2:
A in F
; M . A = (C_Meas M) . A
then reconsider A9 = A as Subset of X ;
for x being ExtReal st x in Svc (M,A9) holds
M . A <= x
proof
let x be
ExtReal;
( x in Svc (M,A9) implies M . A <= x )
assume
x in Svc (
M,
A9)
;
M . A <= x
then consider Aseq being
Covering of
A9,
F such that A3:
x = SUM (vol (M,Aseq))
by Def7;
consider Bseq being
Sep_Sequence of
F such that A4:
A = union (rng Bseq)
and A5:
for
n being
Nat holds
Bseq . n c= Aseq . n
by A2, Th17;
for
n being
Element of
NAT holds
(M * Bseq) . n <= (vol (M,Aseq)) . n
then
SUM (M * Bseq) <= SUM (vol (M,Aseq))
by SUPINF_2:43;
hence
M . A <= x
by A1, A2, A3, A4;
verum
end;
then
M . A is LowerBound of Svc (M,A9)
by XXREAL_2:def 2;
then
M . A <= inf (Svc (M,A9))
by XXREAL_2:def 4;
then A6:
M . A <= (C_Meas M) . A9
by Def8;
(C_Meas M) . A <= M . A
by A2, Th9;
hence
M . A = (C_Meas M) . A
by A6, XXREAL_0:1; verum