let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds COM M is_complete COM S,M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds COM M is_complete COM S,M
let M be sigma_Measure of S; :: thesis: COM M is_complete COM S,M
for A being Subset of X
for B being set st B in COM S,M & A c= B & (COM M) . B = 0. holds
A in COM S,M
proof
let A be
Subset of
X;
:: thesis: for B being set st B in COM S,M & A c= B & (COM M) . B = 0. holds
A in COM S,Mlet B be
set ;
:: thesis: ( B in COM S,M & A c= B & (COM M) . B = 0. implies A in COM S,M )
assume A1:
B in COM S,
M
;
:: thesis: ( not A c= B or not (COM M) . B = 0. or A in COM S,M )
assume A2:
(
A c= B &
(COM M) . B = 0. )
;
:: thesis: A in COM S,M
ex
B1 being
set st
(
B1 in S & ex
C1 being
thin of
M st
A = B1 \/ C1 )
proof
consider B2 being
set such that A3:
(
B2 in S & ex
C2 being
thin of
M st
B = B2 \/ C2 )
by A1, Def4;
consider C2 being
thin of
M such that A4:
B = B2 \/ C2
by A3;
A5:
M . B2 = 0.
by A2, A3, Def6;
consider D2 being
set such that A6:
(
D2 in S &
C2 c= D2 &
M . D2 = 0. )
by Def3;
set C1 =
(A /\ B2) \/ (A /\ C2);
A7:
A =
A /\ (B2 \/ C2)
by A2, A4, XBOOLE_1:28
.=
{} \/ ((A /\ B2) \/ (A /\ C2))
by XBOOLE_1:23
;
set O =
B2 \/ D2;
(
A /\ B2 c= B2 &
A /\ C2 c= C2 )
by XBOOLE_1:17;
then A8:
(
A /\ B2 c= B2 &
A /\ C2 c= D2 )
by A6, XBOOLE_1:1;
A9:
(A /\ B2) \/ (A /\ C2) is
thin of
M
proof
ex
O being
set st
(
O in S &
(A /\ B2) \/ (A /\ C2) c= O &
M . O = 0. )
proof
reconsider O1 =
B2 \/ D2 as
Element of
S by A3, A6, FINSUB_1:def 1;
reconsider B2 =
B2,
D2 =
D2 as
Element of
S by A3, A6;
B10:
M . (B2 \/ D2) <= 0. + 0.
by A5, A6, MEASURE1:64;
A11:
0. <= M . O1
by MEASURE1:def 4;
take
B2 \/ D2
;
:: thesis: ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. )
thus
(
B2 \/ D2 in S &
(A /\ B2) \/ (A /\ C2) c= B2 \/ D2 &
M . (B2 \/ D2) = 0. )
by A8, B10, A11, XBOOLE_1:13, XXREAL_0:1;
:: thesis: verum
end;
hence
(A /\ B2) \/ (A /\ C2) is
thin of
M
by Def3;
:: thesis: verum
end;
take
{}
;
:: thesis: ( {} in S & ex C1 being thin of M st A = {} \/ C1 )
thus
(
{} in S & ex
C1 being
thin of
M st
A = {} \/ C1 )
by A7, A9, PROB_1:10;
:: thesis: verum
end;
hence
A in COM S,
M
by Def4;
:: thesis: verum
end;
hence
COM M is_complete COM S,M
by Def2; :: thesis: verum