:: MEASURE4 semantic presentation

theorem Th1: :: MEASURE4:1

for b₁, b₂, b₃ being R_eal st 0. <=' b₁ & 0. <=' b₂ & 0. <=' b₃ holds
(b₁ + b₂) + b₃ = b₁ + (b₂ + b₃)

proof end;

theorem Th2: :: MEASURE4:2

for b₁, b₂, b₃ being R_eal st not b₁ = -infty & not b₁ = +infty holds
( b₂ + b₁ <=' b₃ iff b₂ <=' b₃ - b₁ )

proof end;

theorem Th3: :: MEASURE4:3

canceled;

theorem Th4: :: MEASURE4:4

for b₁ being set
for b₂ being non empty Subset-Family of b₁
for b₃, b₄ being Function of NAT ,b₂
for b₅ being Element of b₂ st ( for b₆ being Element of NAT holds b₄ . b₆ = b₅ /\ (b₃ . b₆) ) holds
union (rng b₄) = b₅ /\ (union (rng b₃))

proof end;

theorem Th5: :: MEASURE4:5

for b₁ being set
for b₂ being non empty Subset-Family of b₁
for b₃, b₄ being Function of NAT ,b₂ st b₄ . 0 = b₃ . 0 & ( for b₅ being Element of NAT holds b₄ . (b₅ + 1) = (b₃ . (b₅ + 1)) \/ (b₄ . b₅) ) holds
for b₅ being Function of NAT ,b₂ st b₅ . 0 = b₃ . 0 & ( for b₆ being Element of NAT holds b₅ . (b₆ + 1) = (b₃ . (b₆ + 1)) \ (b₄ . b₆) ) holds
union (rng b₃) = union (rng b₅)

proof end;

theorem Th6: :: MEASURE4:6

for b₁ being set holds bool b₁ is sigma_Field_Subset of b₁

proof end;

definition

let c₁ be set ;
let c₂ be Function of NAT , bool c₁;
redefine func rng as rng c₂ -> Subset-Family of a₁;
coherence by RELSET_1:12;

end;

definition

let c₁ be set ;
let c₂, c₃ be non empty set ;
let c₄ be Function of c₁,c₂;
let c₅ be Function of c₂,c₃;
redefine func * as c₅ * c₄ -> Function of a₁,a₃;
coherence

proof end;

end;

theorem Th7: :: MEASURE4:7

for b₁ being set
for b₂, b₃ being R_eal ex b₄ being Function of bool b₁, ExtREAL st
for b₅ being Subset of b₁ holds
( ( b₅ = {} implies b₄ . b₅ = b₂ ) & ( b₅ <> {} implies b₄ . b₅ = b₃ ) )

proof end;

theorem Th8: :: MEASURE4:8

for b₁ being set ex b₂ being Function of bool b₁, ExtREAL st
for b₃ being Subset of b₁ holds b₂ . b₃ = 0.

proof end;

theorem Th9: :: MEASURE4:9

canceled;

theorem Th10: :: MEASURE4:10

canceled;

theorem Th11: :: MEASURE4:11

for b₁ being set ex b₂ being Function of bool b₁, ExtREAL st
( b₂ is nonnegative & b₂ . {} = 0. & ( for b₃, b₄ being Subset of b₁ st b₃ c= b₄ holds
( b₂ . b₃ <=' b₂ . b₄ & ( for b₅ being Function of NAT , bool b₁ holds b₂ . (union (rng b₅)) <=' SUM (b₂ * b₅) ) ) ) )

proof end;

definition

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

end;

:: deftheorem Def1 MEASURE4:def 1 :

:: deftheorem Def2 defines C_Measure MEASURE4:def 2 :

definition

let c₁ be set ;
let c₂ be C_Measure of c₁;
func sigma_Field c₂ -> non empty Subset-Family of a₁ means :Def3: :: MEASURE4:def 3
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff for b₂, b₃ being Subset of a₁ st b₂ c= b₁ & b₃ c= a₁ \ b₁ holds
(a₂ . b₂) + (a₂ . b₃) <=' a₂ . (b₂ \/ b₃) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines sigma_Field MEASURE4:def 3 :

theorem Th12: :: MEASURE4:12

for b₁ being set
for b₂ being C_Measure of b₁
for b₃, b₄ being Subset of b₁ holds b₂ . (b₃ \/ b₄) <=' (b₂ . b₃) + (b₂ . b₄)

proof end;

theorem Th13: :: MEASURE4:13

canceled;

theorem Th14: :: MEASURE4:14

for b₁ being set
for b₂ being C_Measure of b₁
for b₃ being Subset of b₁ holds
( b₃ in sigma_Field b₂ iff for b₄, b₅ being Subset of b₁ st b₄ c= b₃ & b₅ c= b₁ \ b₃ holds
(b₂ . b₄) + (b₂ . b₅) = b₂ . (b₄ \/ b₅) )

proof end;

theorem Th15: :: MEASURE4:15

for b₁ being set
for b₂ being C_Measure of b₁
for b₃, b₄ being Subset of b₁ st b₃ in sigma_Field b₂ & b₄ in sigma_Field b₂ & b₄ misses b₃ holds
b₂ . (b₃ \/ b₄) = (b₂ . b₃) + (b₂ . b₄)

proof end;

theorem Th16: :: MEASURE4:16

for b₁, b₂ being set
for b₃ being C_Measure of b₂ st b₁ in sigma_Field b₃ holds
b₂ \ b₁ in sigma_Field b₃

proof end;

theorem Th17: :: MEASURE4:17

for b₁, b₂, b₃ being set
for b₄ being C_Measure of b₁ st b₂ in sigma_Field b₄ & b₃ in sigma_Field b₄ holds
b₂ \/ b₃ in sigma_Field b₄

proof end;

theorem Th18: :: MEASURE4:18

for b₁, b₂, b₃ being set
for b₄ being C_Measure of b₁ st b₂ in sigma_Field b₄ & b₃ in sigma_Field b₄ holds
b₂ /\ b₃ in sigma_Field b₄

proof end;

theorem Th19: :: MEASURE4:19

for b₁, b₂, b₃ being set
for b₄ being C_Measure of b₁ st b₂ in sigma_Field b₄ & b₃ in sigma_Field b₄ holds
b₂ \ b₃ in sigma_Field b₄

proof end;

theorem Th20: :: MEASURE4:20

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Function of NAT ,b₂
for b₄ being Element of b₂ ex b₅ being Function of NAT ,b₂ st
for b₆ being Element of NAT holds b₅ . b₆ = b₄ /\ (b₃ . b₆)

proof end;

theorem Th21: :: MEASURE4:21

for b₁ being set
for b₂ being C_Measure of b₁ holds sigma_Field b₂ is sigma_Field_Subset of b₁

proof end;

registration

let c₁ be set ;
let c₂ be C_Measure of c₁;
cluster sigma_Field a₂ -> non empty compl-closed sigma_Field_Subset-like ;
coherence by Th21;

end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be N_Sub_fam of c₂;
redefine func union as union c₃ -> Element of a₂;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be C_Measure of c₁;
func sigma_Meas c₂ -> Function of sigma_Field a₂, ExtREAL means :Def4: :: MEASURE4:def 4
for b₁ being Subset of a₁ st b₁ in sigma_Field a₂ holds
a₃ . b₁ = a₂ . b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines sigma_Meas MEASURE4:def 4 :

theorem Th22: :: MEASURE4:22

for b₁ being set
for b₂ being C_Measure of b₁ holds sigma_Meas b₂ is Measure of sigma_Field b₂

proof end;

definition

let c₁ be set ;
let c₂ be C_Measure of c₁;
let c₃ be Element of sigma_Field c₂;
redefine func . as c₂ . c₃ -> R_eal;
coherence by FUNCT_2:7;

end;

theorem Th23: :: MEASURE4:23

for b₁ being set
for b₂ being C_Measure of b₁ holds sigma_Meas b₂ is sigma_Measure of sigma_Field b₂

proof end;

definition

let c₁ be set ;
let c₂ be C_Measure of c₁;
redefine func sigma_Meas as sigma_Meas c₂ -> sigma_Measure of sigma_Field a₂;
coherence by Th23;

end;

theorem Th24: :: MEASURE4:24

for b₁ being set
for b₂ being C_Measure of b₁
for b₃ being Subset of b₁ st b₂ . b₃ = 0. holds
b₃ in sigma_Field b₂

proof end;

theorem Th25: :: MEASURE4:25

for b₁ being set
for b₂ being C_Measure of b₁ holds sigma_Meas b₂ is_complete sigma_Field b₂

proof end;