:: MEASURE2 semantic presentation

theorem Th1: :: MEASURE2:1
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being Function of NAT ,b2 holds b3 * b4 is nonnegative
proof end;

definition
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
mode N_Measure_fam of c2 -> N_Sub_set_fam of a1 means :Def1: :: MEASURE2:def 1
a3 c= a2;
existence
ex b1 being N_Sub_set_fam of c1 st b1 c= c2
proof end;
end;

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

theorem Th2: :: MEASURE2:2
canceled;

theorem Th3: :: MEASURE2:3
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being N_Measure_fam of b2 holds
( meet b3 in b2 & union b3 in b2 )
proof end;

definition
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
let c3 be N_Measure_fam of c2;
redefine func meet as meet c3 -> Element of a2;
coherence
meet c3 is Element of c2 by Th3;
redefine func union as union c3 -> Element of a2;
coherence
union c3 is Element of c2 by Th3;
end;

theorem Th4: :: MEASURE2:4
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2 ex b4 being Function of NAT ,b2 st
( b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds b4 . (b5 + 1) = (b3 . (b5 + 1)) \ (b3 . b5) ) )
proof end;

theorem Th5: :: MEASURE2:5
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2 ex b4 being Function of NAT ,b2 st
( b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds b4 . (b5 + 1) = (b3 . (b5 + 1)) \/ (b4 . b5) ) )
proof end;

theorem Th6: :: MEASURE2:6
for b1 being set
for b2 being non empty Subset-Family of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds b4 . (b5 + 1) = (b3 . (b5 + 1)) \/ (b4 . b5) ) holds
for b5 being set
for b6 being Nat holds
( b5 in b4 . b6 iff ex b7 being Nat st
( b7 <= b6 & b5 in b3 . b7 ) )
proof end;

theorem Th7: :: MEASURE2:7
for b1 being set
for b2 being non empty Subset-Family of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds b4 . (b5 + 1) = (b3 . (b5 + 1)) \/ (b4 . b5) ) holds
for b5, b6 being Nat st b5 < b6 holds
b4 . b5 c= b4 . b6
proof end;

theorem Th8: :: MEASURE2:8
for b1 being set
for b2 being non empty Subset-Family of b1
for b3, b4, b5 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b6 being Element of NAT holds b4 . (b6 + 1) = (b3 . (b6 + 1)) \/ (b4 . b6) ) & b5 . 0 = b3 . 0 & ( for b6 being Element of NAT holds b5 . (b6 + 1) = (b3 . (b6 + 1)) \ (b4 . b6) ) holds
for b6, b7 being Nat st b6 <= b7 holds
b5 . b6 c= b4 . b7
proof end;

theorem Th9: :: MEASURE2:9
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4 being Function of NAT ,b2 ex b5 being Function of NAT ,b2 st
( b5 . 0 = b3 . 0 & ( for b6 being Element of NAT holds b5 . (b6 + 1) = (b3 . (b6 + 1)) \ (b4 . b6) ) )
proof end;

theorem Th10: :: MEASURE2:10
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2 ex b4 being Function of NAT ,b2 st
( b4 . 0 = {} & ( for b5 being Element of NAT holds b4 . (b5 + 1) = (b3 . 0) \ (b3 . b5) ) )
proof end;

theorem Th11: :: MEASURE2:11
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4, b5 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b6 being Element of NAT holds b4 . (b6 + 1) = (b3 . (b6 + 1)) \/ (b4 . b6) ) & b5 . 0 = b3 . 0 & ( for b6 being Element of NAT holds b5 . (b6 + 1) = (b3 . (b6 + 1)) \ (b4 . b6) ) holds
for b6, b7 being Nat st b6 < b7 holds
b5 . b6 misses b5 . b7
proof end;

theorem Th12: :: MEASURE2:12
canceled;

theorem Th13: :: MEASURE2:13
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being N_Measure_fam of b2
for b5 being Function of NAT ,b2 st b4 = rng b5 holds
b3 . (union b4) <=' SUM (b3 * b5)
proof end;

theorem Th14: :: MEASURE2:14
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being N_Measure_fam of b2 ex b4 being Function of NAT ,b2 st b3 = rng b4
proof end;

theorem Th15: :: MEASURE2:15
for b1, b2 being Function st b2 . 0 = {} & ( for b3 being Element of NAT holds
( b2 . (b3 + 1) = (b1 . 0) \ (b1 . b3) & b1 . (b3 + 1) c= b1 . b3 ) ) holds
for b3 being Element of NAT holds b2 . b3 c= b2 . (b3 + 1)
proof end;

theorem Th16: :: MEASURE2:16
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being N_Measure_fam of b2 st ( for b5 being set st b5 in b4 holds
b5 is measure_zero of b3 ) holds
union b4 is measure_zero of b3
proof end;

theorem Th17: :: MEASURE2:17
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being N_Measure_fam of b2 st ex b5 being set st
( b5 in b4 & b5 is measure_zero of b3 ) holds
meet b4 is measure_zero of b3
proof end;

theorem Th18: :: MEASURE2:18
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being N_Measure_fam of b2 st ( for b5 being set st b5 in b4 holds
b5 is measure_zero of b3 ) holds
meet b4 is measure_zero of b3
proof end;

definition
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
let c3 be N_Measure_fam of c2;
attr a3 is non-decreasing means :Def2: :: MEASURE2:def 2
ex b1 being Function of NAT ,a2 st
( a3 = rng b1 & ( for b2 being Element of NAT holds b1 . b2 c= b1 . (b2 + 1) ) );
end;

:: deftheorem Def2 defines non-decreasing MEASURE2:def 2 :
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being N_Measure_fam of b2 holds
( b3 is non-decreasing iff ex b4 being Function of NAT ,b2 st
( b3 = rng b4 & ( for b5 being Element of NAT holds b4 . b5 c= b4 . (b5 + 1) ) ) );

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

definition
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
let c3 be N_Measure_fam of c2;
attr a3 is non-increasing means :: MEASURE2:def 3
ex b1 being Function of NAT ,a2 st
( a3 = rng b1 & ( for b2 being Element of NAT holds b1 . (b2 + 1) c= b1 . b2 ) );
end;

:: deftheorem Def3 defines non-increasing MEASURE2:def 3 :
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being N_Measure_fam of b2 holds
( b3 is non-increasing iff ex b4 being Function of NAT ,b2 st
( b3 = rng b4 & ( for b5 being Element of NAT holds b4 . (b5 + 1) c= b4 . b5 ) ) );

registration
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
cluster non-increasing N_Measure_fam of a2;
existence
ex b1 being N_Measure_fam of c2 st b1 is non-increasing
proof end;
end;

theorem Th19: :: MEASURE2:19
canceled;

theorem Th20: :: MEASURE2:20
canceled;

theorem Th21: :: MEASURE2:21
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = {} & ( for b5 being Element of NAT holds
( b4 . (b5 + 1) = (b3 . 0) \ (b3 . b5) & b3 . (b5 + 1) c= b3 . b5 ) ) holds
rng b4 is non-decreasing N_Measure_fam of b2
proof end;

theorem Th22: :: MEASURE2:22
for b1 being Function st ( for b2 being Element of NAT holds b1 . b2 c= b1 . (b2 + 1) ) holds
for b2, b3 being Nat st b3 <= b2 holds
b1 . b3 c= b1 . b2
proof end;

theorem Th23: :: MEASURE2:23
for b1, b2 being Function st b2 . 0 = b1 . 0 & ( for b3 being Element of NAT holds
( b2 . (b3 + 1) = (b1 . (b3 + 1)) \ (b1 . b3) & b1 . b3 c= b1 . (b3 + 1) ) ) holds
for b3, b4 being Nat st b3 < b4 holds
b2 . b3 misses b2 . b4
proof end;

theorem Th24: :: MEASURE2:24
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds
( b4 . (b5 + 1) = (b3 . (b5 + 1)) \ (b3 . b5) & b3 . b5 c= b3 . (b5 + 1) ) ) holds
union (rng b4) = union (rng b3)
proof end;

theorem Th25: :: MEASURE2:25
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds
( b4 . (b5 + 1) = (b3 . (b5 + 1)) \ (b3 . b5) & b3 . b5 c= b3 . (b5 + 1) ) ) holds
b4 is Sep_Sequence of b2
proof end;

theorem Th26: :: MEASURE2:26
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3, b4 being Function of NAT ,b2 st b4 . 0 = b3 . 0 & ( for b5 being Element of NAT holds
( b4 . (b5 + 1) = (b3 . (b5 + 1)) \ (b3 . b5) & b3 . b5 c= b3 . (b5 + 1) ) ) holds
( b3 . 0 = b4 . 0 & ( for b5 being Element of NAT holds b3 . (b5 + 1) = (b4 . (b5 + 1)) \/ (b3 . b5) ) )
proof end;

theorem Th27: :: MEASURE2:27
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being Function of NAT ,b2 st ( for b5 being Element of NAT holds b4 . b5 c= b4 . (b5 + 1) ) holds
b3 . (union (rng b4)) = sup (rng (b3 * b4))
proof end;