:: MEASURE2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MEASURE2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for F being Function of NAT ,S holds M * F is nonnegative
proof end;

definition
let X be set ;
let S be sigma_Field_Subset of X;
mode N_Measure_fam of S -> N_Sub_set_fam of X means :Def1: :: MEASURE2:def 1
it c= S;
existence
ex b1 being N_Sub_set_fam of X st b1 c= S
proof end;
end;

:: deftheorem Def1 defines N_Measure_fam MEASURE2:def 1 :
for X being set
for S being sigma_Field_Subset of X
for b3 being N_Sub_set_fam of X holds
( b3 is N_Measure_fam of S iff b3 c= S );

theorem :: MEASURE2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: MEASURE2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset 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 sigma_Field_Subset 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 Th3;
:: original: union
redefine func union T -> Element of S;
coherence
union T is Element of S by Th3;
end;

theorem Th4: :: MEASURE2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N being Function of NAT ,S ex F being Function of NAT ,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (N . n) ) )
proof end;

theorem Th5: :: MEASURE2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N being Function of NAT ,S ex F being Function of NAT ,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \/ (F . n) ) )
proof end;

theorem Th6: :: MEASURE2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being non empty Subset-Family of X
for N, F being Function of NAT ,S st F . 0 = N . 0 & ( for n being Element of 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 Th7: :: MEASURE2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being non empty Subset-Family of X
for N, F being Function of NAT ,S st F . 0 = N . 0 & ( for n being Element of 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 Th8: :: MEASURE2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being non empty Subset-Family of X
for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of 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 Th9: :: MEASURE2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, G being Function of NAT ,S ex F being Function of NAT ,S st
( F . 0 = N . 0 & ( for n being Element of NAT holds F . (n + 1) = (N . (n + 1)) \ (G . n) ) )
proof end;

theorem :: MEASURE2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N being Function of NAT ,S ex F being Function of NAT ,S st
( F . 0 = {} & ( for n being Element of NAT holds F . (n + 1) = (N . 0) \ (N . n) ) )
proof end;

theorem Th11: :: MEASURE2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, G, F being Function of NAT ,S st G . 0 = N . 0 & ( for n being Element of NAT holds G . (n + 1) = (N . (n + 1)) \/ (G . n) ) & F . 0 = N . 0 & ( for n being Element of 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 :: MEASURE2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: MEASURE2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for T being N_Measure_fam of S
for F being Function of NAT ,S st T = rng F holds
M . (union T) <=' SUM (M * F)
proof end;

theorem Th14: :: MEASURE2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for T being N_Measure_fam of S ex F being Function of NAT ,S st T = rng F
proof end;

theorem Th15: :: MEASURE2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N, F being Function st F . 0 = {} & ( for n being Element of NAT holds
( F . (n + 1) = (N . 0) \ (N . n) & N . (n + 1) c= N . n ) ) holds
for n being Element of NAT holds F . n c= F . (n + 1)
proof end;

theorem :: MEASURE2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset 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 Th17: :: MEASURE2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset 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
proof end;

theorem :: MEASURE2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset 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;

definition
let X be set ;
let S be sigma_Field_Subset of X;
let IT be N_Measure_fam of S;
attr IT is non-decreasing means :Def2: :: MEASURE2:def 2
 ex F being Function of NAT ,S st
( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) );
end;

:: deftheorem Def2 defines non-decreasing MEASURE2:def 2 :
for X being set
for S being sigma_Field_Subset of X
for IT being N_Measure_fam of S holds
( IT is non-decreasing iff ex F being Function of NAT ,S st
( IT = rng F & ( for n being Element of NAT holds F . n c= F . (n + 1) ) ) );

registration
let X be set ;
let S be sigma_Field_Subset of X;
cluster non-decreasing N_Measure_fam of S;
existence
ex b1 being N_Measure_fam of S st b1 is non-decreasing
proof end;
end;

definition
let X be set ;
let S be sigma_Field_Subset of X;
let IT be N_Measure_fam of S;
attr IT is non-increasing means :: MEASURE2:def 3
 ex F being Function of NAT ,S st
( IT = rng F & ( for n being Element of NAT holds F . (n + 1) c= F . n ) );
end;

:: deftheorem defines non-increasing MEASURE2:def 3 :
for X being set
for S being sigma_Field_Subset of X
for IT being N_Measure_fam of S holds
( IT is non-increasing iff ex F being Function of NAT ,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 sigma_Field_Subset of X;
cluster non-increasing N_Measure_fam of S;
existence
ex b1 being N_Measure_fam of S st b1 is non-increasing
proof end;
end;

theorem :: MEASURE2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: MEASURE2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, F being Function of NAT ,S st F . 0 = {} & ( for n being Element of 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 Th22: :: MEASURE2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Function st ( for n being Element of NAT holds N . n c= N . (n + 1) ) holds
for m, n being Nat st n <= m holds
N . n c= N . m
proof end;

theorem Th23: :: MEASURE2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N, F being Function 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
for n, m being Nat st n < m holds
F . n misses F . m
proof end;

theorem Th24: :: MEASURE2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, F being Function of NAT ,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
union (rng F) = union (rng N)
proof end;

theorem Th25: :: MEASURE2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, F being Function of NAT ,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
F is Sep_Sequence of S
proof end;

theorem :: MEASURE2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for N, F being Function of NAT ,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:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for F being Function of NAT ,S st ( for n being Element of NAT holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))
proof end;