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

::

:: Received July 3, 1991

:: Copyright (c) 1991-2021 Association of Mizar Users

theorem :: MEASURE2:1

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S holds M * F is V92() by MEASURE1:25;

for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S holds M * F is V92() by MEASURE1:25;

definition

let X be set ;

let S be SigmaField of X;

existence

ex b_{1} being N_Sub_set_fam of X st b_{1} c= S

end;
let S be SigmaField of X;

existence

ex b

proof end;

:: deftheorem Def1 defines N_Measure_fam MEASURE2:def 1 :

for X being set

for S being SigmaField of X

for b_{3} being N_Sub_set_fam of X holds

( b_{3} is N_Measure_fam of S iff b_{3} c= S );

for X being set

for S being SigmaField of X

for b

( b

theorem Th2: :: MEASURE2:2

for X being set

for S being SigmaField of X

for T being N_Measure_fam of S holds

( meet T in S & union T in S )

for S being SigmaField of X

for T being N_Measure_fam of S holds

( meet T in S & union T in S )

proof end;

definition

let X be set ;

let S be SigmaField of X;

let T be N_Measure_fam of S;

:: original: meet

redefine func meet T -> Element of S;

coherence

meet T is Element of S by Th2;

:: original: union

redefine func union T -> Element of S;

coherence

union T is Element of S by Th2;

end;
let S be SigmaField of X;

let T be N_Measure_fam of S;

:: original: meet

redefine func meet T -> Element of S;

coherence

meet T is Element of S by Th2;

:: original: union

redefine func union T -> Element of S;

coherence

union T is Element of S by Th2;

theorem Th3: :: MEASURE2:3

for X being set

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )

proof end;

theorem Th4: :: MEASURE2:4

for X being set

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )

proof end;

theorem Th5: :: MEASURE2:5

for X being set

for S being non empty Subset-Family of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

for S being non empty Subset-Family of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for r being set

for n being Nat holds

( r in F . n iff ex k being Nat st

( k <= n & r in N . k ) )

proof end;

theorem Th6: :: MEASURE2:6

for X being set

for S being non empty Subset-Family of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for n, m being Nat st n < m holds

F . n c= F . m

for S being non empty Subset-Family of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) holds

for n, m being Nat st n < m holds

F . n c= F . m

proof end;

theorem Th7: :: MEASURE2:7

for X being set

for S being non empty Subset-Family of X

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

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

F . n c= G . m

for S being non empty Subset-Family of X

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

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

F . n c= G . m

proof end;

theorem Th8: :: MEASURE2:8

for X being set

for S being SigmaField of X

for N, G being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )

for S being SigmaField of X

for N, G being sequence of S ex F being sequence of S st

( F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )

proof end;

theorem :: MEASURE2:9

for X being set

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )

for S being SigmaField of X

for N being sequence of S ex F being sequence of S st

( F . 0 = {} & ( for n being Nat holds F . (n + 1) = (N . 0) \ (N . n) ) )

proof end;

theorem Th10: :: MEASURE2:10

for X being set

for S being SigmaField of X

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

for S being SigmaField of X

for N, G, F being sequence of S st G . 0 = N . 0 & ( for n being Nat holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Nat holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

proof end;

theorem Th11: :: MEASURE2:11

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S

for F being sequence of S st T = rng F holds

M . (union T) <= SUM (M * F)

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S

for F being sequence of S st T = rng F holds

M . (union T) <= SUM (M * F)

proof end;

theorem Th12: :: MEASURE2:12

for X being set

for S being SigmaField of X

for T being N_Measure_fam of S ex F being sequence of S st T = rng F

for S being SigmaField of X

for T being N_Measure_fam of S ex F being sequence of S st T = rng F

proof end;

theorem Th13: :: MEASURE2:13

for N, F being Function st F . 0 = {} & ( for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds

for n being Nat holds F . n c= F . (n + 1)

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds

for n being Nat holds F . n c= F . (n + 1)

proof end;

theorem :: MEASURE2:14

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ( for A being set st A in T holds

A is measure_zero of M ) holds

union T is measure_zero of M

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ( for A being set st A in T holds

A is measure_zero of M ) holds

union T is measure_zero of M

proof end;

theorem :: MEASURE2:15

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ex A being set st

( A in T & A is measure_zero of M ) holds

meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3;

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ex A being set st

( A in T & A is measure_zero of M ) holds

meet T is measure_zero of M by MEASURE1:36, SETFAM_1:3;

theorem :: MEASURE2:16

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ( for A being set st A in T holds

A is measure_zero of M ) holds

meet T is measure_zero of M

for S being SigmaField of X

for M being sigma_Measure of S

for T being N_Measure_fam of S st ( for A being set st A in T holds

A is measure_zero of M ) holds

meet T is measure_zero of M

proof end;

:: deftheorem Def2 defines non-decreasing MEASURE2:def 2 :

for X being set

for S being SigmaField of X

for IT being N_Measure_fam of S holds

( IT is non-decreasing iff ex F being sequence of S st

( IT = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) ) );

for X being set

for S being SigmaField of X

for IT being N_Measure_fam of S holds

( IT is non-decreasing iff ex F being sequence of S st

( IT = rng F & ( for n being Nat holds F . n c= F . (n + 1) ) ) );

registration

let X be set ;

let S be SigmaField of X;

existence

ex b_{1} being N_Measure_fam of S st b_{1} is non-decreasing

end;
let S be SigmaField of X;

existence

ex b

proof end;

:: deftheorem defines non-increasing MEASURE2:def 3 :

for X being set

for S being SigmaField of X

for IT being N_Measure_fam of S holds

( IT is non-increasing iff ex F being sequence of S st

( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) );

for X being set

for S being SigmaField of X

for IT being N_Measure_fam of S holds

( IT is non-increasing iff ex F being sequence of S st

( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) ) );

registration

let X be set ;

let S be SigmaField of X;

existence

ex b_{1} being N_Measure_fam of S st b_{1} is non-increasing

end;
let S be SigmaField of X;

existence

ex b

proof end;

theorem :: MEASURE2:17

for X being set

for S being SigmaField of X

for N, F being sequence of S st F . 0 = {} & ( for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds

rng F is non-decreasing N_Measure_fam of S

for S being SigmaField of X

for N, F being sequence of S st F . 0 = {} & ( for n being Nat holds

( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds

rng F is non-decreasing N_Measure_fam of S

proof end;

theorem Th18: :: MEASURE2:18

for N being Function st ( for n being Nat holds N . n c= N . (n + 1) ) holds

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

N . n c= N . m

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

N . n c= N . m

proof end;

theorem Th19: :: MEASURE2:19

for N, F being Function st F . 0 = N . 0 & ( for n being Nat holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

for n, m being Nat st n < m holds

F . n misses F . m

proof end;

theorem Th20: :: MEASURE2:20

for X being set

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

union (rng F) = union (rng N)

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

union (rng F) = union (rng N)

proof end;

theorem Th21: :: MEASURE2:21

for X being set

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

F is Sep_Sequence of S

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Nat holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

F is Sep_Sequence of S

proof end;

theorem :: MEASURE2:22

for X being set

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Element of NAT holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )

for S being SigmaField of X

for N, F being sequence of S st F . 0 = N . 0 & ( for n being Element of NAT holds

( F . (n + 1) = (N . (n + 1)) \ (N . n) & N . n c= N . (n + 1) ) ) holds

( N . 0 = F . 0 & ( for n being Element of NAT holds N . (n + 1) = (F . (n + 1)) \/ (N . n) ) )

proof end;

theorem :: MEASURE2:23

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . n c= F . (n + 1) ) holds

M . (union (rng F)) = sup (rng (M * F))

for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of S st ( for n being Nat holds F . n c= F . (n + 1) ) holds

M . (union (rng F)) = sup (rng (M * F))

proof end;