:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama

::

:: Received April 7, 2009

:: Copyright (c) 2009-2019 Association of Mizar Users

:: In the theorem below, the notion "summable" means in MESFUNC9, not in SUPINF_2

theorem Th3: :: MEASURE8:3

for seq, seq1, seq2 being ExtREAL_sequence st seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) holds

( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )

( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )

proof end;

registration

let X be set ;

let F be Field_Subset of X;

ex b_{1} being sequence of F st b_{1} is disjoint_valued

end;
let F be Field_Subset of X;

cluster non empty Relation-like omega -defined F -valued Function-like V30( omega ) quasi_total disjoint_valued for Element of bool [:omega,F:];

existence ex b

proof end;

definition

let X be set ;

let F be Field_Subset of X;

ex b_{1} being FinSequence of bool X st

for k being Nat st k in dom b_{1} holds

b_{1} . k in F

end;
let F be Field_Subset of X;

mode FinSequence of F -> FinSequence of bool X means :Def1: :: MEASURE8:def 1

for k being Nat st k in dom it holds

it . k in F;

existence for k being Nat st k in dom it holds

it . k in F;

ex b

for k being Nat st k in dom b

b

proof end;

:: deftheorem Def1 defines FinSequence MEASURE8:def 1 :

for X being set

for F being Field_Subset of X

for b_{3} being FinSequence of bool X holds

( b_{3} is FinSequence of F iff for k being Nat st k in dom b_{3} holds

b_{3} . k in F );

for X being set

for F being Field_Subset of X

for b

( b

b

registration

let X be set ;

let F be Field_Subset of X;

ex b_{1} being FinSequence of F st b_{1} is disjoint_valued

end;
let F be Field_Subset of X;

cluster Relation-like omega -defined bool X -valued Function-like FinSequence-like disjoint_valued for FinSequence of F;

existence ex b

proof end;

definition

let X be set ;

let F be Field_Subset of X;

mode Sep_FinSequence of F is disjoint_valued FinSequence of F;

end;
let F be Field_Subset of X;

mode Sep_FinSequence of F is disjoint_valued FinSequence of F;

definition
end;

definition

let X be set ;

let F be Field_Subset of X;

ex b_{1} being SetSequence of X st

for n being Nat holds b_{1} . n in F

end;
let F be Field_Subset of X;

mode Set_Sequence of F -> SetSequence of X means :Def2: :: MEASURE8:def 2

for n being Nat holds it . n in F;

existence for n being Nat holds it . n in F;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def2 defines Set_Sequence MEASURE8:def 2 :

for X being set

for F being Field_Subset of X

for b_{3} being SetSequence of X holds

( b_{3} is Set_Sequence of F iff for n being Nat holds b_{3} . n in F );

for X being set

for F being Field_Subset of X

for b

( b

definition

let X be set ;

let A be Subset of X;

let F be Field_Subset of X;

existence

ex b_{1} being Set_Sequence of F st A c= union (rng b_{1})

end;
let A be Subset of X;

let F be Field_Subset of X;

existence

ex b

proof end;

:: deftheorem Def3 defines Covering MEASURE8:def 3 :

for X being set

for A being Subset of X

for F being Field_Subset of X

for b_{4} being Set_Sequence of F holds

( b_{4} is Covering of A,F iff A c= union (rng b_{4}) );

for X being set

for A being Subset of X

for F being Field_Subset of X

for b

( b

definition

let X be set ;

let F be Field_Subset of X;

let FSets be Set_Sequence of F;

let n be Nat;

:: original: .

redefine func FSets . n -> Element of F;

correctness

coherence

FSets . n is Element of F;

by Def2;

end;
let F be Field_Subset of X;

let FSets be Set_Sequence of F;

let n be Nat;

:: original: .

redefine func FSets . n -> Element of F;

correctness

coherence

FSets . n is Element of F;

by Def2;

Lm1: for X being set

for F being Field_Subset of X holds NAT --> X is Set_Sequence of F

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let Sets be SetSequence of X;

ex b_{1} being sequence of (Funcs (NAT,(bool X))) st

for n being Nat holds b_{1} . n is Covering of Sets . n,F

end;
let F be Field_Subset of X;

let Sets be SetSequence of X;

mode Covering of Sets,F -> sequence of (Funcs (NAT,(bool X))) means :Def4: :: MEASURE8:def 4

for n being Nat holds it . n is Covering of Sets . n,F;

existence for n being Nat holds it . n is Covering of Sets . n,F;

ex b

for n being Nat holds b

proof end;

:: deftheorem Def4 defines Covering MEASURE8:def 4 :

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for b_{4} being sequence of (Funcs (NAT,(bool X))) holds

( b_{4} is Covering of Sets,F iff for n being Nat holds b_{4} . n is Covering of Sets . n,F );

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for b

( b

definition

let X be set ;

let F be Field_Subset of X;

let M be Measure of F;

let FSets be Set_Sequence of F;

ex b_{1} being ExtREAL_sequence st

for n being Nat holds b_{1} . n = M . (FSets . n)

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Nat holds b_{1} . n = M . (FSets . n) ) & ( for n being Nat holds b_{2} . n = M . (FSets . n) ) holds

b_{1} = b_{2}

end;
let F be Field_Subset of X;

let M be Measure of F;

let FSets be Set_Sequence of F;

func vol (M,FSets) -> ExtREAL_sequence means :Def5: :: MEASURE8:def 5

for n being Nat holds it . n = M . (FSets . n);

existence for n being Nat holds it . n = M . (FSets . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines vol MEASURE8:def 5 :

for X being set

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F

for b_{5} being ExtREAL_sequence holds

( b_{5} = vol (M,FSets) iff for n being Nat holds b_{5} . n = M . (FSets . n) );

for X being set

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F

for b

( b

theorem Th4: :: MEASURE8:4

for X being set

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let Sets be SetSequence of X;

let Cvr be Covering of Sets,F;

let n be Nat;

:: original: .

redefine func Cvr . n -> Covering of Sets . n,F;

correctness

coherence

Cvr . n is Covering of Sets . n,F;

by Def4;

end;
let F be Field_Subset of X;

let Sets be SetSequence of X;

let Cvr be Covering of Sets,F;

let n be Nat;

:: original: .

redefine func Cvr . n -> Covering of Sets . n,F;

correctness

coherence

Cvr . n is Covering of Sets . n,F;

by Def4;

definition

let X be set ;

let F be Field_Subset of X;

let Sets be SetSequence of X;

let M be Measure of F;

let Cvr be Covering of Sets,F;

ex b_{1} being ExtREAL_sequence st

for n being Nat holds b_{1} . n = SUM (vol (M,(Cvr . n)))

for b_{1}, b_{2} being ExtREAL_sequence st ( for n being Nat holds b_{1} . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds b_{2} . n = SUM (vol (M,(Cvr . n))) ) holds

b_{1} = b_{2}

end;
let F be Field_Subset of X;

let Sets be SetSequence of X;

let M be Measure of F;

let Cvr be Covering of Sets,F;

func Volume (M,Cvr) -> ExtREAL_sequence means :Def6: :: MEASURE8:def 6

for n being Nat holds it . n = SUM (vol (M,(Cvr . n)));

existence for n being Nat holds it . n = SUM (vol (M,(Cvr . n)));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines Volume MEASURE8:def 6 :

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for M being Measure of F

for Cvr being Covering of Sets,F

for b_{6} being ExtREAL_sequence holds

( b_{6} = Volume (M,Cvr) iff for n being Nat holds b_{6} . n = SUM (vol (M,(Cvr . n))) );

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for M being Measure of F

for Cvr being Covering of Sets,F

for b

( b

theorem Th5: :: MEASURE8:5

for X being set

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X

for n being Nat

for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X

for n being Nat

for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let M be Measure of F;

let A be Subset of X;

ex b_{1} being Subset of ExtREAL st

for x being R_eal holds

( x in b_{1} iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) )

for b_{1}, b_{2} being Subset of ExtREAL st ( for x being R_eal holds

( x in b_{1} iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds

( x in b_{2} iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) holds

b_{1} = b_{2}

end;
let F be Field_Subset of X;

let M be Measure of F;

let A be Subset of X;

func Svc (M,A) -> Subset of ExtREAL means :Def7: :: MEASURE8:def 7

for x being R_eal holds

( x in it iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) );

existence for x being R_eal holds

( x in it iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) );

ex b

for x being R_eal holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def7 defines Svc MEASURE8:def 7 :

for X being set

for F being Field_Subset of X

for M being Measure of F

for A being Subset of X

for b_{5} being Subset of ExtREAL holds

( b_{5} = Svc (M,A) iff for x being R_eal holds

( x in b_{5} iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) );

for X being set

for F being Field_Subset of X

for M being Measure of F

for A being Subset of X

for b

( b

( x in b

registration

let X be set ;

let A be Subset of X;

let F be Field_Subset of X;

let M be Measure of F;

coherence

not Svc (M,A) is empty

end;
let A be Subset of X;

let F be Field_Subset of X;

let M be Measure of F;

coherence

not Svc (M,A) is empty

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let M be Measure of F;

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

for A being Subset of X holds b_{1} . A = inf (Svc (M,A))

for b_{1}, b_{2} being Function of (bool X),ExtREAL st ( for A being Subset of X holds b_{1} . A = inf (Svc (M,A)) ) & ( for A being Subset of X holds b_{2} . A = inf (Svc (M,A)) ) holds

b_{1} = b_{2}

end;
let F be Field_Subset of X;

let M be Measure of F;

func C_Meas M -> Function of (bool X),ExtREAL means :Def8: :: MEASURE8:def 8

for A being Subset of X holds it . A = inf (Svc (M,A));

existence for A being Subset of X holds it . A = inf (Svc (M,A));

ex b

for A being Subset of X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines C_Meas MEASURE8:def 8 :

for X being set

for F being Field_Subset of X

for M being Measure of F

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

( b_{4} = C_Meas M iff for A being Subset of X holds b_{4} . A = inf (Svc (M,A)) );

for X being set

for F being Field_Subset of X

for M being Measure of F

for b

( b

definition
end;

definition

let X be set ;

let F be Field_Subset of X;

let Sets be SetSequence of X;

let Cvr be Covering of Sets,F;

ex b_{1} being Covering of union (rng Sets),F st

for n being Nat holds b_{1} . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)

for b_{1}, b_{2} being Covering of union (rng Sets),F st ( for n being Nat holds b_{1} . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds b_{2} . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) holds

b_{1} = b_{2}

end;
let F be Field_Subset of X;

let Sets be SetSequence of X;

let Cvr be Covering of Sets,F;

func On Cvr -> Covering of union (rng Sets),F means :Def10: :: MEASURE8:def 10

for n being Nat holds it . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n);

existence for n being Nat holds it . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines On MEASURE8:def 10 :

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for Cvr being Covering of Sets,F

for b_{5} being Covering of union (rng Sets),F holds

( b_{5} = On Cvr iff for n being Nat holds b_{5} . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) );

for X being set

for F being Field_Subset of X

for Sets being SetSequence of X

for Cvr being Covering of Sets,F

for b

( b

theorem Th6: :: MEASURE8:6

for X being set

for F being Field_Subset of X

for M being Measure of F

for k being Nat ex m being Nat st

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m

for F being Field_Subset of X

for M being Measure of F

for k being Nat ex m being Nat st

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m

proof end;

theorem Th7: :: MEASURE8:7

for X being set

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X

for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))

proof end;

theorem Th8: :: MEASURE8:8

for X being set

for F being Field_Subset of X

for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

for F being Field_Subset of X

for A being Subset of X st A in F holds

(A,({} X)) followed_by ({} X) is Covering of A,F

proof end;

theorem Th9: :: MEASURE8:9

for X being set

for F being Field_Subset of X

for M being Measure of F

for A being set st A in F holds

(C_Meas M) . A <= M . A

for F being Field_Subset of X

for M being Measure of F

for A being set st A in F holds

(C_Meas M) . A <= M . A

proof end;

theorem Th10: :: MEASURE8:10

for X being set

for F being Field_Subset of X

for M being Measure of F holds C_Meas M is nonnegative

for F being Field_Subset of X

for M being Measure of F holds C_Meas M is nonnegative

proof end;

theorem Th12: :: MEASURE8:12

for X being set

for F being Field_Subset of X

for M being Measure of F

for A, B being Subset of X st A c= B holds

(C_Meas M) . A <= (C_Meas M) . B

for F being Field_Subset of X

for M being Measure of F

for A, B being Subset of X st A c= B holds

(C_Meas M) . A <= (C_Meas M) . B

proof end;

Lm2: for X being set

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds

(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

proof end;

theorem Th13: :: MEASURE8:13

for X being set

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

for F being Field_Subset of X

for M being Measure of F

for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)

proof end;

theorem Th14: :: MEASURE8:14

for X being set

for F being Field_Subset of X

for M being Measure of F holds C_Meas M is C_Measure of X

for F being Field_Subset of X

for M being Measure of F holds C_Meas M is C_Measure of X

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let M be Measure of F;

:: original: C_Meas

redefine func C_Meas M -> C_Measure of X;

correctness

coherence

C_Meas M is C_Measure of X;

by Th14;

end;
let F be Field_Subset of X;

let M be Measure of F;

:: original: C_Meas

redefine func C_Meas M -> C_Measure of X;

correctness

coherence

C_Meas M is C_Measure of X;

by Th14;

definition

let X be set ;

let F be Field_Subset of X;

let M be Measure of F;

end;
let F be Field_Subset of X;

let M be Measure of F;

attr M is completely-additive means :: MEASURE8:def 11

for FSets being Sep_Sequence of F st union (rng FSets) in F holds

SUM (M * FSets) = M . (union (rng FSets));

for FSets being Sep_Sequence of F st union (rng FSets) in F holds

SUM (M * FSets) = M . (union (rng FSets));

:: deftheorem defines completely-additive MEASURE8:def 11 :

for X being set

for F being Field_Subset of X

for M being Measure of F holds

( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds

SUM (M * FSets) = M . (union (rng FSets)) );

for X being set

for F being Field_Subset of X

for M being Measure of F holds

( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds

SUM (M * FSets) = M . (union (rng FSets)) );

theorem Th15: :: MEASURE8:15

for X being set

for F being Field_Subset of X

for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F

for F being Field_Subset of X

for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F

proof end;

theorem Th16: :: MEASURE8:16

for X being set

for F being Field_Subset of X

for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

for F being Field_Subset of X

for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F

proof end;

theorem Th17: :: MEASURE8:17

for X being set

for F being Field_Subset of X

for A being Subset of X

for CA being Covering of A,F st A in F holds

ex FSets being Sep_Sequence of F st

( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )

for F being Field_Subset of X

for A being Subset of X

for CA being Covering of A,F st A in F holds

ex FSets being Sep_Sequence of F st

( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )

proof end;

theorem Th18: :: MEASURE8:18

for X being 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

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

proof end;

theorem Th19: :: MEASURE8:19

for X being set

for A being Subset of X

for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds

A in sigma_Field C

for A being Subset of X

for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds

A in sigma_Field C

proof end;

theorem Th20: :: MEASURE8:20

for X being set

for F being Field_Subset of X

for M being Measure of F holds F c= sigma_Field (C_Meas M)

for F being Field_Subset of X

for M being Measure of F holds F c= sigma_Field (C_Meas M)

proof end;

theorem Th21: :: MEASURE8:21

for X being set

for F being Field_Subset of X

for FSets being Set_Sequence of F

for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence

for F being Field_Subset of X

for FSets being Set_Sequence of F

for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let FSets be Set_Sequence of F;

let g be Function of F,ExtREAL;

:: original: *

redefine func g * FSets -> ExtREAL_sequence;

correctness

coherence

FSets * g is ExtREAL_sequence;

by Th21;

end;
let F be Field_Subset of X;

let FSets be Set_Sequence of F;

let g be Function of F,ExtREAL;

:: original: *

redefine func g * FSets -> ExtREAL_sequence;

correctness

coherence

FSets * g is ExtREAL_sequence;

by Th21;

theorem Th22: :: MEASURE8:22

for X being set

for S being SigmaField of X

for SSets being SetSequence of S

for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence

for S being SigmaField of X

for SSets being SetSequence of S

for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence

proof end;

definition

let X be set ;

let S be SigmaField of X;

let SSets be SetSequence of S;

let g be Function of S,ExtREAL;

:: original: *

redefine func g * SSets -> ExtREAL_sequence;

correctness

coherence

SSets * g is ExtREAL_sequence;

by Th22;

end;
let S be SigmaField of X;

let SSets be SetSequence of S;

let g be Function of S,ExtREAL;

:: original: *

redefine func g * SSets -> ExtREAL_sequence;

correctness

coherence

SSets * g is ExtREAL_sequence;

by Th22;

theorem Th23: :: MEASURE8:23

for F, G being sequence of ExtREAL

for n being Nat st ( for m being Nat st m <= n holds

F . m <= G . m ) holds

(Ser F) . n <= (Ser G) . n

for n being Nat st ( for m being Nat st m <= n holds

F . m <= G . m ) holds

(Ser F) . n <= (Ser G) . n

proof end;

theorem Th24: :: MEASURE8:24

for X being set

for C being C_Measure of X

for seq being Sep_Sequence of (sigma_Field C) holds

( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )

for C being C_Measure of X

for seq being Sep_Sequence of (sigma_Field C) holds

( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )

proof end;

theorem :: MEASURE8:25

for X being set

for C being C_Measure of X

for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C

for C being C_Measure of X

for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C

proof end;

theorem Th26: :: MEASURE8:26

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-descending holds

lim (M * SSets) = M . (lim SSets)

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-descending holds

lim (M * SSets) = M . (lim SSets)

proof end;

theorem :: MEASURE8:27

for X being set

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-descending holds

M * FSets is non-decreasing

proof end;

theorem :: MEASURE8:28

for X being set

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-ascending holds

M * FSets is non-increasing

for F being Field_Subset of X

for M being Measure of F

for FSets being Set_Sequence of F st FSets is non-ascending holds

M * FSets is non-increasing

proof end;

theorem Th29: :: MEASURE8:29

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-descending holds

M * SSets is non-decreasing

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-descending holds

M * SSets is non-decreasing

proof end;

theorem Th30: :: MEASURE8:30

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending holds

M * SSets is non-increasing

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending holds

M * SSets is non-increasing

proof end;

theorem :: MEASURE8:31

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds

lim (M * SSets) = M . (lim SSets)

for S being SigmaField of X

for M being sigma_Measure of S

for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds

lim (M * SSets) = M . (lim SSets)

proof end;

definition

let X be set ;

let F be Field_Subset of X;

let S be SigmaField of X;

let m be Measure of F;

let M be sigma_Measure of S;

end;
let F be Field_Subset of X;

let S be SigmaField of X;

let m be Measure of F;

let M be sigma_Measure of S;

:: deftheorem defines is_extension_of MEASURE8:def 12 :

for X being set

for F being Field_Subset of X

for S being SigmaField of X

for m being Measure of F

for M being sigma_Measure of S holds

( M is_extension_of m iff for A being set st A in F holds

M . A = m . A );

for X being set

for F being Field_Subset of X

for S being SigmaField of X

for m being Measure of F

for M being sigma_Measure of S holds

( M is_extension_of m iff for A being set st A in F holds

M . A = m . A );

theorem :: MEASURE8:32

for X being non empty set

for F being Field_Subset of X

for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds

m is completely-additive

for F being Field_Subset of X

for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds

m is completely-additive

proof end;

theorem Th33: :: MEASURE8:33

for X being non empty set

for F being Field_Subset of X

for m being Measure of F st m is completely-additive holds

ex M being sigma_Measure of (sigma F) st

( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )

for F being Field_Subset of X

for m being Measure of F st m is completely-additive holds

ex M being sigma_Measure of (sigma F) st

( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )

proof end;

theorem Th34: :: MEASURE8:34

for X being set

for F being Field_Subset of X

for M being Measure of F

for k being Nat

for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds

M . ((Partial_Union FSets) . k) < +infty

for F being Field_Subset of X

for M being Measure of F

for k being Nat

for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds

M . ((Partial_Union FSets) . k) < +infty

proof end;

theorem :: MEASURE8:35

for X being non empty set

for F being Field_Subset of X

for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

for F being Field_Subset of X

for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st

( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds

for M being sigma_Measure of (sigma F) st M is_extension_of m holds

M = (sigma_Meas (C_Meas m)) | (sigma F)

proof end;