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

begin

theorem :: MEASURE4:1

canceled;

theorem :: MEASURE4:2

canceled;

theorem :: MEASURE4:3

canceled;

theorem Th4: :: MEASURE4:4

for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT,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 Th5: :: MEASURE4:5

for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being Function of NAT,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)

proof end;

theorem Th6: :: MEASURE4:6

for X being set holds bool X is SigmaField of X

proof end;

theorem :: MEASURE4:7

canceled;

theorem :: MEASURE4:8

canceled;

theorem :: MEASURE4:9

canceled;

theorem :: MEASURE4:10

canceled;

theorem :: MEASURE4:11

canceled;

definition

let X be set ;
canceled;
mode C_Measure of X -> Function of (bool X),ExtREAL means :Def2: :: MEASURE4:def 2
( it is nonnegative & it is zeroed & ( for A, B being Subset of X st A c= B holds
( it . A <= it . B & ( for F being Function of NAT,(bool X) holds it . (union (rng F)) <= SUM (it * F) ) ) ) );
existence
ex b₁ being Function of (bool X),ExtREAL st
( b₁ is nonnegative & b₁ is zeroed & ( for A, B being Subset of X st A c= B holds
( b₁ . A <= b₁ . B & ( for F being Function of NAT,(bool X) holds b₁ . (union (rng F)) <= SUM (b₁ * F) ) ) ) )

proof end;

end;

:: deftheorem MEASURE4:def 1 :
canceled;

:: deftheorem Def2 defines C_Measure MEASURE4:def 2 :
for X being set
for b₂ being Function of (bool X),ExtREAL holds
( b₂ is C_Measure of X iff ( b₂ is nonnegative & b₂ is zeroed & ( for A, B being Subset of X st A c= B holds
( b₂ . A <= b₂ . B & ( for F being Function of NAT,(bool X) holds b₂ . (union (rng F)) <= SUM (b₂ * F) ) ) ) ) );

definition

let X be set ;
let C be C_Measure of X;
func sigma_Field C -> non empty Subset-Family of X means :Def3: :: MEASURE4:def 3
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 b₁ being non empty Subset-Family of X st
for A being Subset of X holds
( A in b₁ 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 b₁, b₂ being non empty Subset-Family of X st ( for A being Subset of X holds
( A in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines sigma_Field MEASURE4:def 3 :
for X being set
for C being C_Measure of X
for b₃ being non empty Subset-Family of X holds
( b₃ = sigma_Field C iff for A being Subset of X holds
( A in b₃ 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 Th12: :: MEASURE4:12

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 :: MEASURE4:13

canceled;

theorem Th14: :: MEASURE4:14

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 Th15: :: MEASURE4:15

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 Th16: :: MEASURE4:16

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 Th17: :: MEASURE4:17

for X, A, B 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 Th18: :: MEASURE4:18

for X, A, B 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 Th19: :: MEASURE4:19

for X, A, B 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 Th20: :: MEASURE4:20

for X being set
for S being SigmaField of X
for N being Function of NAT,S
for A being Element of S ex F being Function of NAT,S st
for n being Element of NAT holds F . n = A /\ (N . n)

proof end;

theorem Th21: :: MEASURE4:21

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 Th21;

end;

definition

let X be set ;
let S be SigmaField of X;
let A be N_Sub_fam of S;
:: original: union
redefine func union A -> Element of S;
coherence
union A is Element of S

proof end;

end;

definition

let X be set ;
let C be C_Measure of X;
func sigma_Meas C -> Function of (sigma_Field C),ExtREAL means :Def4: :: MEASURE4:def 4
for A being Subset of X st A in sigma_Field C holds
it . A = C . A;
existence
ex b₁ being Function of (sigma_Field C),ExtREAL st
for A being Subset of X st A in sigma_Field C holds
b₁ . A = C . A

proof end;

uniqueness
for b₁, b₂ being Function of (sigma_Field C),ExtREAL st ( for A being Subset of X st A in sigma_Field C holds
b₁ . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds
b₂ . A = C . A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines sigma_Meas MEASURE4:def 4 :
for X being set
for C being C_Measure of X
for b₃ being Function of (sigma_Field C),ExtREAL holds
( b₃ = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds
b₃ . A = C . A );

theorem Th22: :: MEASURE4:22

for X being set
for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C)

proof end;

theorem Th23: :: MEASURE4:23

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 V85() sigma-additive ;
coherence
( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th23;

end;

theorem Th24: :: MEASURE4:24

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:25

for X being set
for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C

proof end;