:: Properties of Caratheodory's Measure
:: by J\'ozef Bia{\l}as
::
:: Received June 25, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users


theorem Th1: :: MEASURE4:1
for X being set
for S being non empty Subset-Family of X
for F, G being sequence of 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 end;

theorem Th2: :: MEASURE4:2
for X being set
for S being non empty Subset-Family of X
for F, G being sequence of S st G . 0 = F . 0 & ( for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being sequence of S st H . 0 = F . 0 & ( for n being Nat holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)
proof end;

theorem Th3: :: MEASURE4:3
for X being set holds bool X is SigmaField of X
proof end;

definition
let X be set ;
mode C_Measure of X -> Function of (bool X),ExtREAL means :Def1: :: MEASURE4:def 1
( it is V92() & it is zeroed & ( for A, B being Subset of X st A c= B holds
( it . A <= it . B & ( for F being sequence of (bool X) holds it . (union (rng F)) <= SUM (it * F) ) ) ) );
existence
ex b1 being Function of (bool X),ExtREAL st
( b1 is V92() & b1 is zeroed & ( for A, B being Subset of X st A c= B holds
( b1 . A <= b1 . B & ( for F being sequence of (bool X) holds b1 . (union (rng F)) <= SUM (b1 * F) ) ) ) )
proof 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 V92() & b2 is zeroed & ( for A, B being Subset of X st A c= B holds
( b2 . A <= b2 . B & ( for F being sequence of (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 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 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 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 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 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 end;

theorem Th8: :: MEASURE4:8
for A, B, X 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 end;

theorem Th9: :: MEASURE4:9
for A, B, X 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 end;

theorem Th10: :: MEASURE4:10
for A, B, X 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 end;

theorem Th11: :: MEASURE4:11
for X being set
for S being SigmaField of X
for N being sequence of S
for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)
proof 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 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_Measure_fam of S;
:: original: union
redefine func union A -> Element of S;
coherence
union A is Element of S by MEASURE2:def 1, MEASURE1:def 5;
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 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 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 end;

:: WP: Caratheodory's Theorem
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 end;

registration
let X be set ;
let C be C_Measure of X;
cluster sigma_Meas C -> zeroed V92() 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 end;

theorem :: MEASURE4:16
for X being set
for C being C_Measure of X holds sigma_Meas C is complete
proof end;