:: MEASURE4 semantic presentation

theorem Th1: :: MEASURE4:1

for x, y, z being R_eal st 0. <=' x & 0. <=' y & 0. <=' z holds
(x + y) + z = x + (y + z)

proof end;

theorem Th2: :: MEASURE4:2

for x, y, z being R_eal st not x = -infty & not x = +infty holds
( y + x <=' z iff y <=' z - x )

proof end;

theorem :: MEASURE4:3

canceled;

theorem Th4: :: MEASURE4:4

for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT ,S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))

proof end;

theorem Th5: :: MEASURE4:5

for X being set
for S being non empty Subset-Family of X
for F, G being Function of NAT ,S st G . 0 = F . 0 & ( for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being Function of NAT ,S st H . 0 = F . 0 & ( for n being Element of NAT holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)

proof end;

theorem Th6: :: MEASURE4:6

for X being set holds bool X is sigma_Field_Subset of X

proof end;

definition

let X be set ;
let F be Function of NAT , bool X;
:: original: rng
redefine func rng F -> Subset-Family of X;
coherence by RELSET_1:12;

end;

definition

let Y be set ;
let X, Z be non empty set ;
let F be Function of Y,X;
let M be Function of X,Z;
:: original: *
redefine func M * F -> Function of Y,Z;
coherence

proof end;

end;

theorem Th7: :: MEASURE4:7

for X being set
for a, b being R_eal ex M being Function of bool X, ExtREAL st
for A being Subset of X holds
( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

proof end;

theorem Th8: :: MEASURE4:8

for X being set ex M being Function of bool X, ExtREAL st
for A being Subset of X holds M . A = 0.

proof end;

theorem :: MEASURE4:9

canceled;

theorem :: MEASURE4:10

canceled;

theorem Th11: :: MEASURE4:11

for X being set ex M being Function of bool X, ExtREAL st
( M is nonnegative & M . {} = 0. & ( for A, B being Subset of X st A c= B holds
( M . A <=' M . B & ( for F being Function of NAT , bool X holds M . (union (rng F)) <=' SUM (M * F) ) ) ) )

proof end;

definition

let X be set ;
canceled;
mode C_Measure of X -> Function of bool X, ExtREAL means :Def2: :: MEASURE4:def 2
( it is nonnegative & it . {} = 0. & ( for A, B being Subset of X st A c= B holds
( it . A <=' it . B & ( for F being Function of NAT , bool X holds it . (union (rng F)) <=' SUM (it * F) ) ) ) );
existence by Th11;

end;

:: deftheorem MEASURE4:def 1 :

:: deftheorem Def2 defines C_Measure MEASURE4:def 2 :

definition

let X be set ;
let C be C_Measure of X;
func sigma_Field C -> non empty Subset-Family of X means :Def3: :: MEASURE4:def 3
for A being Subset of X holds
( A in it iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <=' C . (W \/ Z) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines sigma_Field MEASURE4:def 3 :

theorem Th12: :: MEASURE4:12

for X being set
for C being C_Measure of X
for W, Z being Subset of X holds C . (W \/ Z) <=' (C . W) + (C . Z)

proof end;

theorem :: MEASURE4:13

canceled;

theorem Th14: :: MEASURE4:14

for X being set
for C being C_Measure of X
for A being Subset of X holds
( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )

proof end;

theorem Th15: :: MEASURE4:15

for X being set
for C being C_Measure of X
for W, Z being Subset of X st W in sigma_Field C & Z in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)

proof end;

theorem Th16: :: MEASURE4:16

for A, X being set
for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C

proof end;

theorem Th17: :: MEASURE4:17

for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \/ B in sigma_Field C

proof end;

theorem Th18: :: MEASURE4:18

for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A /\ B in sigma_Field C

proof end;

theorem Th19: :: MEASURE4:19

for X, A, B being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \ B in sigma_Field C

proof end;

theorem Th20: :: MEASURE4:20

for X being set
for S being sigma_Field_Subset of X
for N being Function of NAT ,S
for A being Element of S ex F being Function of NAT ,S st
for n being Element of NAT holds F . n = A /\ (N . n)

proof end;

theorem Th21: :: MEASURE4:21

for X being set
for C being C_Measure of X holds sigma_Field C is sigma_Field_Subset of X

proof end;

registration

let X be set ;
let C be C_Measure of X;
cluster sigma_Field C -> non empty compl-closed sigma_Field_Subset-like ;
coherence by Th21;

end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let A be N_Sub_fam of S;
:: original: union
redefine func union A -> Element of S;
coherence

proof end;

end;

definition

let X be set ;
let C be C_Measure of X;
func sigma_Meas C -> Function of sigma_Field C, ExtREAL means :Def4: :: MEASURE4:def 4
for A being Subset of X st A in sigma_Field C holds
it . A = C . A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines sigma_Meas MEASURE4:def 4 :

theorem Th22: :: MEASURE4:22

for X being set
for C being C_Measure of X holds sigma_Meas C is Measure of sigma_Field C

proof end;

definition

let X be set ;
let C be C_Measure of X;
let A be Element of sigma_Field C;
:: original: .
redefine func C . A -> R_eal;
coherence by FUNCT_2:7;

end;

theorem Th23: :: MEASURE4:23

for X being set
for C being C_Measure of X holds sigma_Meas C is sigma_Measure of sigma_Field C

proof end;

definition

let X be set ;
let C be C_Measure of X;
:: original: sigma_Meas
redefine func sigma_Meas C -> sigma_Measure of sigma_Field C;
coherence by Th23;

end;

theorem Th24: :: MEASURE4:24

for X being set
for C being C_Measure of X
for A being Subset of X st C . A = 0. holds
A in sigma_Field C

proof end;

theorem :: MEASURE4:25

for X being set
for C being C_Measure of X holds sigma_Meas C is_complete sigma_Field C

proof end;