:: by J\'ozef Bia{\l}as

::

:: Received June 25, 1992

:: Copyright (c) 1992-2019 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))

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)

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;

definition

let X be set ;

ex b_{1} being Function of (bool X),ExtREAL st

( b_{1} is V92() & b_{1} is zeroed & ( for A, B being Subset of X st A c= B holds

( b_{1} . A <= b_{1} . B & ( for F being sequence of (bool X) holds b_{1} . (union (rng F)) <= SUM (b_{1} * F) ) ) ) )

end;
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 ( 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) ) ) ) );

ex b

( b

( b

proof end;

:: deftheorem Def1 defines C_Measure MEASURE4:def 1 :

for X being set

for b_{2} being Function of (bool X),ExtREAL holds

( b_{2} is C_Measure of X iff ( b_{2} is V92() & b_{2} is zeroed & ( for A, B being Subset of X st A c= B holds

( b_{2} . A <= b_{2} . B & ( for F being sequence of (bool X) holds b_{2} . (union (rng F)) <= SUM (b_{2} * F) ) ) ) ) );

for X being set

for b

( b

( b

definition

let X be set ;

let C be C_Measure of X;

ex b_{1} being non empty Subset-Family of X st

for A being Subset of X holds

( A in b_{1} 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 b_{1}, b_{2} being non empty Subset-Family of X st ( for A being Subset of X holds

( A in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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) );

ex b

for A being Subset of X holds

( A in b

(C . W) + (C . Z) <= C . (W \/ Z) )

proof end;

uniqueness for b

( A in b

(C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds

( A in b

(C . W) + (C . Z) <= C . (W \/ Z) ) ) holds

b

proof end;

:: deftheorem Def2 defines sigma_Field MEASURE4:def 2 :

for X being set

for C being C_Measure of X

for b_{3} being non empty Subset-Family of X holds

( b_{3} = sigma_Field C iff for A being Subset of X holds

( A in b_{3} 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 X being set

for C being C_Measure of X

for b

( b

( A in b

(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)

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) )

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)

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

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

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

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)

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;

registration

let X be set ;

let C be C_Measure of X;

coherence

( sigma_Field C is sigma-additive & sigma_Field C is compl-closed & not sigma_Field C is empty ) by Th12;

end;
let C be C_Measure of X;

coherence

( sigma_Field C is sigma-additive & sigma_Field C is compl-closed & not sigma_Field C is empty ) by Th12;

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

definition

let X be set ;

let C be C_Measure of X;

ex b_{1} being Function of (sigma_Field C),ExtREAL st

for A being Subset of X st A in sigma_Field C holds

b_{1} . A = C . A

for b_{1}, b_{2} being Function of (sigma_Field C),ExtREAL st ( for A being Subset of X st A in sigma_Field C holds

b_{1} . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds

b_{2} . A = C . A ) holds

b_{1} = b_{2}

end;
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 for A being Subset of X st A in sigma_Field C holds

it . A = C . A;

ex b

for A being Subset of X st A in sigma_Field C holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines sigma_Meas MEASURE4:def 3 :

for X being set

for C being C_Measure of X

for b_{3} being Function of (sigma_Field C),ExtREAL holds

( b_{3} = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds

b_{3} . A = C . A );

for X being set

for C being C_Measure of X

for b

( b

b

:: Caratheodory's Theorem

registration

let X be set ;

let C be C_Measure of X;

coherence

( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th14;

end;
let C be C_Measure of X;

coherence

( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th14;

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

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;