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

::

:: Received October 15, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

registration
end;

theorem Th4: :: MEASURE1:4

for X being set

for S being non empty Subset-Family of X holds

( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )

for S being non empty Subset-Family of X holds

( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )

proof end;

definition

let X be set ;

let IT be Subset-Family of X;

( IT is compl-closed iff for A being set st A in IT holds

X \ A in IT )

end;
let IT be Subset-Family of X;

redefine attr IT is compl-closed means :Def1: :: MEASURE1:def 1

for A being set st A in IT holds

X \ A in IT;

compatibility for A being set st A in IT holds

X \ A in IT;

( IT is compl-closed iff for A being set st A in IT holds

X \ A in IT )

proof end;

:: deftheorem Def1 defines compl-closed MEASURE1:def 1 :

for X being set

for IT being Subset-Family of X holds

( IT is compl-closed iff for A being set st A in IT holds

X \ A in IT );

for X being set

for IT being Subset-Family of X holds

( IT is compl-closed iff for A being set st A in IT holds

X \ A in IT );

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is cup-closed & b_{1} is compl-closed holds

b_{1} is cap-closed

for b_{1} being Subset-Family of X st b_{1} is cap-closed & b_{1} is compl-closed holds

b_{1} is cup-closed

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is compl-closed & b_{1} is cap-closed holds

b_{1} is diff-closed

end;
coherence

for b

b

proof end;

theorem :: MEASURE1:6

for X being set

for S being Field_Subset of X

for A, B being set st A in S & B in S holds

A \ B in S by FINSUB_1:def 3;

for S being Field_Subset of X

for A, B being set st A in S & B in S holds

A \ B in S by FINSUB_1:def 3;

theorem :: MEASURE1:7

definition

let X be non empty set ;

let F be Function of X,ExtREAL;

( F is nonnegative iff for A being Element of X holds 0. <= F . A ) by SUPINF_2:39;

end;
let F be Function of X,ExtREAL;

:: original: nonnegative

redefine attr F is nonnegative means :Def2: :: MEASURE1:def 2

for A being Element of X holds 0. <= F . A;

compatibility redefine attr F is nonnegative means :Def2: :: MEASURE1:def 2

for A being Element of X holds 0. <= F . A;

( F is nonnegative iff for A being Element of X holds 0. <= F . A ) by SUPINF_2:39;

:: deftheorem Def2 defines nonnegative MEASURE1:def 2 :

for X being non empty set

for F being Function of X,ExtREAL holds

( F is nonnegative iff for A being Element of X holds 0. <= F . A );

for X being non empty set

for F being Function of X,ExtREAL holds

( F is nonnegative iff for A being Element of X holds 0. <= F . A );

:: deftheorem Def3 defines additive MEASURE1:def 3 :

for X being set

for S being Field_Subset of X

for F being Function of S,ExtREAL holds

( F is additive iff for A, B being Element of S st A misses B holds

F . (A \/ B) = (F . A) + (F . B) );

for X being set

for S being Field_Subset of X

for F being Function of S,ExtREAL holds

( F is additive iff for A, B being Element of S st A misses B holds

F . (A \/ B) = (F . A) + (F . B) );

registration

let X be set ;

let S be Field_Subset of X;

ex b_{1} being Function of S,ExtREAL st

( b_{1} is V89() & b_{1} is additive & b_{1} is zeroed )

end;
let S be Field_Subset of X;

cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() additive for Element of bool [:S,ExtREAL:];

existence ex b

( b

proof end;

definition

let X be set ;

let S be Field_Subset of X;

mode Measure of S is zeroed V89() additive Function of S,ExtREAL;

end;
let S be Field_Subset of X;

mode Measure of S is zeroed V89() additive Function of S,ExtREAL;

theorem Th8: :: MEASURE1:8

for X being set

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S st A c= B holds

M . A <= M . B

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S st A c= B holds

M . A <= M . B

proof end;

theorem Th9: :: MEASURE1:9

for X being set

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

proof end;

registration

let X be set ;

existence

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

( not b_{1} is empty & b_{1} is compl-closed & b_{1} is cap-closed )

end;
existence

ex b

( not b

proof end;

definition

let X be set ;

let S be non empty cup-closed Subset-Family of X;

let A, B be Element of S;

:: original: \/

redefine func A \/ B -> Element of S;

coherence

A \/ B is Element of S by FINSUB_1:def 1;

end;
let S be non empty cup-closed Subset-Family of X;

let A, B be Element of S;

:: original: \/

redefine func A \/ B -> Element of S;

coherence

A \/ B is Element of S by FINSUB_1:def 1;

definition

let X be set ;

let S be Field_Subset of X;

let A, B be Element of S;

:: original: /\

redefine func A /\ B -> Element of S;

coherence

A /\ B is Element of S by FINSUB_1:def 2;

:: original: \

redefine func A \ B -> Element of S;

coherence

A \ B is Element of S by FINSUB_1:def 3;

end;
let S be Field_Subset of X;

let A, B be Element of S;

:: original: /\

redefine func A /\ B -> Element of S;

coherence

A /\ B is Element of S by FINSUB_1:def 2;

:: original: \

redefine func A \ B -> Element of S;

coherence

A \ B is Element of S by FINSUB_1:def 3;

theorem Th10: :: MEASURE1:10

for X being set

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

for S being Field_Subset of X

for M being Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

proof end;

theorem :: MEASURE1:11

definition

let X be set ;

let S be Field_Subset of X;

let M be Measure of S;

existence

ex b_{1} being Element of S st M . b_{1} = 0.

end;
let S be Field_Subset of X;

let M be Measure of S;

existence

ex b

proof end;

:: deftheorem Def4 defines measure_zero MEASURE1:def 4 :

for X being set

for S being Field_Subset of X

for M being Measure of S

for b_{4} being Element of S holds

( b_{4} is measure_zero of M iff M . b_{4} = 0. );

for X being set

for S being Field_Subset of X

for M being Measure of S

for b

( b

theorem :: MEASURE1:12

for X being set

for S being Field_Subset of X

for M being Measure of S

for A being Element of S

for B being measure_zero of M st A c= B holds

A is measure_zero of M

for S being Field_Subset of X

for M being Measure of S

for A being Element of S

for B being measure_zero of M st A c= B holds

A is measure_zero of M

proof end;

theorem :: MEASURE1:13

for X being set

for S being Field_Subset of X

for M being Measure of S

for A, B being measure_zero of M holds

( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

for S being Field_Subset of X

for M being Measure of S

for A, B being measure_zero of M holds

( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

proof end;

theorem :: MEASURE1:14

for X being set

for S being Field_Subset of X

for M being Measure of S

for A being Element of S

for B being measure_zero of M holds

( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

for S being Field_Subset of X

for M being Measure of S

for A being Element of S

for B being measure_zero of M holds

( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

proof end;

::

:: sigma_Field Subset of X and sigma_additive nonnegative measure

::

:: sigma_Field Subset of X and sigma_additive nonnegative measure

::

registration

let X be set ;

existence

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

( not b_{1} is empty & b_{1} is V53() )

end;
existence

ex b

( not b

proof end;

theorem Th17: :: MEASURE1:17

for X being set

for A, B, C being Subset of X ex F being Function of NAT,(bool X) st

( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds

F . n = C ) )

for A, B, C being Subset of X ex F being Function of NAT,(bool X) st

( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds

F . n = C ) )

proof end;

theorem Th19: :: MEASURE1:19

for X being set

for A, B being Subset of X ex F being Function of NAT,(bool X) st

( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds

F . n = B ) )

for A, B being Subset of X ex F being Function of NAT,(bool X) st

( rng F = {A,B} & F . 0 = A & ( for n being Element of NAT st 0 < n holds

F . n = B ) )

proof end;

definition

let X be set ;

let IT be Subset-Family of X;

end;
let IT be Subset-Family of X;

attr IT is sigma-additive means :Def5: :: MEASURE1:def 5

for M being N_Sub_set_fam of X st M c= IT holds

union M in IT;

for M being N_Sub_set_fam of X st M c= IT holds

union M in IT;

:: deftheorem Def5 defines sigma-additive MEASURE1:def 5 :

for X being set

for IT being Subset-Family of X holds

( IT is sigma-additive iff for M being N_Sub_set_fam of X st M c= IT holds

union M in IT );

for X being set

for IT being Subset-Family of X holds

( IT is sigma-additive iff for M being N_Sub_set_fam of X st M c= IT holds

union M in IT );

registration

let X be set ;

existence

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

( not b_{1} is empty & b_{1} is compl-closed & b_{1} is sigma-additive )

end;
existence

ex b

( not b

proof end;

registration

let X be set ;

coherence

for b_{1} being Subset-Family of X st b_{1} is compl-closed & b_{1} is sigma-multiplicative holds

b_{1} is sigma-additive

for b_{1} being Subset-Family of X st b_{1} is compl-closed & b_{1} is sigma-additive holds

b_{1} is sigma-multiplicative

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration
end;

theorem Th22: :: MEASURE1:22

for X being set

for S being non empty Subset-Family of X holds

( ( ( for A being set st A in S holds

X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds

meet M in S ) ) iff S is SigmaField of X )

for S being non empty Subset-Family of X holds

( ( ( for A being set st A in S holds

X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds

meet M in S ) ) iff S is SigmaField of X )

proof end;

registration

let X be set ;

let S be SigmaField of X;

ex b_{1} being Function of NAT,S st b_{1} is disjoint_valued

end;
let S be SigmaField of X;

cluster Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) disjoint_valued for Element of bool [:NAT,S:];

existence ex b

proof end;

definition
end;

definition

let X be set ;

let S be SigmaField of X;

let F be Function of NAT,S;

:: original: rng

redefine func rng F -> non empty Subset-Family of X;

coherence

rng F is non empty Subset-Family of X

end;
let S be SigmaField of X;

let F be Function of NAT,S;

:: original: rng

redefine func rng F -> non empty Subset-Family of X;

coherence

rng F is non empty Subset-Family of X

proof end;

theorem Th23: :: MEASURE1:23

for X being set

for S being SigmaField of X

for F being Function of NAT,S holds rng F is N_Sub_set_fam of X

for S being SigmaField of X

for F being Function of NAT,S holds rng F is N_Sub_set_fam of X

proof end;

theorem Th24: :: MEASURE1:24

for X being set

for S being SigmaField of X

for F being Function of NAT,S holds union (rng F) is Element of S

for S being SigmaField of X

for F being Function of NAT,S holds union (rng F) is Element of S

proof end;

theorem Th25: :: MEASURE1:25

for Y, S being non empty set

for F being Function of Y,S

for M being Function of S,ExtREAL st M is V89() holds

M * F is V89()

for F being Function of Y,S

for M being Function of S,ExtREAL st M is V89() holds

M * F is V89()

proof end;

theorem Th26: :: MEASURE1:26

for X being set

for S being SigmaField of X

for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

for S being SigmaField of X

for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

proof end;

theorem :: MEASURE1:27

theorem Th28: :: MEASURE1:28

for X being set

for S being SigmaField of X ex M being Function of S,ExtREAL st

for A being Element of S holds M . A = 0.

for S being SigmaField of X ex M being Function of S,ExtREAL st

for A being Element of S holds M . A = 0.

proof end;

definition

let X be set ;

let S be SigmaField of X;

let F be Function of S,ExtREAL;

end;
let S be SigmaField of X;

let F be Function of S,ExtREAL;

attr F is sigma-additive means :Def6: :: MEASURE1:def 6

for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));

for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));

:: deftheorem Def6 defines sigma-additive MEASURE1:def 6 :

for X being set

for S being SigmaField of X

for F being Function of S,ExtREAL holds

( F is sigma-additive iff for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s)) );

for X being set

for S being SigmaField of X

for F being Function of S,ExtREAL holds

( F is sigma-additive iff for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s)) );

registration

let X be set ;

let S be SigmaField of X;

ex b_{1} being Function of S,ExtREAL st

( b_{1} is V89() & b_{1} is sigma-additive & b_{1} is zeroed )

end;
let S be SigmaField of X;

cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() sigma-additive for Element of bool [:S,ExtREAL:];

existence ex b

( b

proof end;

definition

let X be set ;

let S be SigmaField of X;

mode sigma_Measure of S is zeroed V89() sigma-additive Function of S,ExtREAL;

end;
let S be SigmaField of X;

mode sigma_Measure of S is zeroed V89() sigma-additive Function of S,ExtREAL;

registration

let X be set ;

coherence

for b_{1} being non empty Subset-Family of X st b_{1} is sigma-additive & b_{1} is compl-closed holds

b_{1} is cup-closed
;

end;
coherence

for b

b

theorem :: MEASURE1:30

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A misses B holds

M . (A \/ B) = (M . A) + (M . B)

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A misses B holds

M . (A \/ B) = (M . A) + (M . B)

proof end;

theorem Th31: :: MEASURE1:31

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A c= B holds

M . A <= M . B

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A c= B holds

M . A <= M . B

proof end;

theorem :: MEASURE1:32

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S st A c= B & M . A < +infty holds

M . (B \ A) = (M . B) - (M . A)

proof end;

theorem Th33: :: MEASURE1:33

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)

proof end;

theorem :: MEASURE1:34

for X being set

for S being SigmaField of X

for M being sigma_Measure of S holds

( {} in S & X in S & ( for A, B being set st A in S & B in S holds

( X \ A in S & A \/ B in S & A /\ B in S ) ) ) by Def1, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1:4, PROB_1:5;

for S being SigmaField of X

for M being sigma_Measure of S holds

( {} in S & X in S & ( for A, B being set st A in S & B in S holds

( X \ A in S & A \/ B in S & A /\ B in S ) ) ) by Def1, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1:4, PROB_1:5;

theorem :: MEASURE1:35

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Sub_set_fam of X st ( for A being set st A in T holds

A in S ) holds

( union T in S & meet T in S )

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Sub_set_fam of X st ( for A being set st A in T holds

A in S ) holds

( union T in S & meet T in S )

proof end;

definition

let X be set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

existence

ex b_{1} being Element of S st M . b_{1} = 0.

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

existence

ex b

proof end;

:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for b_{4} being Element of S holds

( b_{4} is measure_zero of M iff M . b_{4} = 0. );

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

theorem :: MEASURE1:36

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for B being measure_zero of M st A c= B holds

A is measure_zero of M

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for B being measure_zero of M st A c= B holds

A is measure_zero of M

proof end;

theorem :: MEASURE1:37

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being measure_zero of M holds

( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

for S being SigmaField of X

for M being sigma_Measure of S

for A, B being measure_zero of M holds

( A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M )

proof end;

theorem :: MEASURE1:38

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for B being measure_zero of M holds

( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for B being measure_zero of M holds

( M . (A \/ B) = M . A & M . (A /\ B) = 0. & M . (A \ B) = M . A )

proof end;

:: Field Subset of X and nonnegative measure

::