:: MEASURE1 semantic presentation

theorem Th1: :: MEASURE1:1

for b₁, b₂ being set holds union {b₁,b₂,{} } = union {b₁,b₂}

proof end;

theorem Th2: :: MEASURE1:2

canceled;

theorem Th3: :: MEASURE1:3

canceled;

theorem Th4: :: MEASURE1:4

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

proof end;

theorem Th5: :: MEASURE1:5

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

proof end;

theorem Th6: :: MEASURE1:6

canceled;

theorem Th7: :: MEASURE1:7

for b₁ being set
for b₂, b₃ being Subset of b₁ holds {b₂,b₃} is Subset-Family of b₁

proof end;

theorem Th8: :: MEASURE1:8

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ holds {b₂,b₃,b₄} is non empty Subset-Family of b₁

proof end;

theorem Th9: :: MEASURE1:9

for b₁ being set holds {{} } is Subset-Family of b₁

proof end;

scheme :: MEASURE1:sch 1
s1{ F₁() -> set , P₁[ set ] } :

ex b₁ being non empty Subset-Family of F₁() st
for b₂ being set holds
( b₂ in b₁ iff ( b₂ c= F₁() & P₁[b₂] ) )

provided

E7: ex b₁ being set st
( b₁ c= F₁() & P₁[b₁] )

proof end;

notation

let c₁ be set ;
let c₂ be non empty Subset-Family of c₁;
synonym c₁ \ c₂ for COMPLEMENT c₂;

end;

registration

let c₁ be set ;
let c₂ be non empty Subset-Family of c₁;
cluster a₁ \ a₂ -> non empty ;
coherence

proof end;

end;

theorem Th10: :: MEASURE1:10

canceled;

theorem Th11: :: MEASURE1:11

canceled;

theorem Th12: :: MEASURE1:12

canceled;

theorem Th13: :: MEASURE1:13

canceled;

theorem Th14: :: MEASURE1:14

canceled;

theorem Th15: :: MEASURE1:15

for b₁ being set
for b₂ being non empty Subset-Family of b₁ holds
( meet b₂ = b₁ \ (union (b₁ \ b₂)) & union b₂ = b₁ \ (meet (b₁ \ b₂)) )

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
canceled;
canceled;
redefine attr a₂ is compl-closed means :Def3: :: MEASURE1:def 3
for b₁ being set st b₁ in a₂ holds
a₁ \ b₁ in a₂;
compatibility

proof end;

end;

:: deftheorem Def1 MEASURE1:def 1 :

:: deftheorem Def2 MEASURE1:def 2 :

:: deftheorem Def3 defines compl-closed MEASURE1:def 3 :

theorem Th16: :: MEASURE1:16

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ is cup-closed & b₂ is compl-closed holds
b₂ is cap-closed

proof end;

registration

let c₁ be set ;
cluster cup-closed compl-closed -> cap-closed Element of bool (bool a₁);
coherence by Th16;
cluster cap-closed compl-closed -> cup-closed Element of bool (bool a₁);
coherence

proof end;

end;

theorem Th17: :: MEASURE1:17

for b₁ being set
for b₂ being Field_Subset of b₁ holds b₂ = b₁ \ b₂

proof end;

theorem Th18: :: MEASURE1:18

for b₁, b₂ being set holds
( b₂ is Field_Subset of b₁ iff ex b₃ being non empty Subset-Family of b₁ st
( b₂ = b₃ & ( for b₄ being set st b₄ in b₃ holds
( b₁ \ b₄ in b₃ & ( for b₅, b₆ being set st b₅ in b₃ & b₆ in b₃ holds
b₅ \/ b₆ in b₃ ) ) ) ) )

proof end;

theorem Th19: :: MEASURE1:19

for b₁ being set
for b₂ being non empty Subset-Family of b₁ holds
( b₂ is Field_Subset of b₁ iff for b₃ being set st b₃ in b₂ holds
( b₁ \ b₃ in b₂ & ( for b₄, b₅ being set st b₄ in b₂ & b₅ in b₂ holds
b₄ /\ b₅ in b₂ ) ) )

proof end;

theorem Th20: :: MEASURE1:20

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

proof end;

theorem Th21: :: MEASURE1:21

for b₁ being set
for b₂ being Field_Subset of b₁ holds
( {} in b₂ & b₁ in b₂ ) by PROB_1:10, PROB_1:11;

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, ExtREAL ;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> R_eal;
coherence by FUNCT_2:7;

end;

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, ExtREAL ;
redefine attr a₂ is nonnegative means :Def4: :: MEASURE1:def 4
for b₁ being Element of a₁ holds 0. <=' a₂ . b₁;
compatibility by SUPINF_2:58;

end;

:: deftheorem Def4 defines nonnegative MEASURE1:def 4 :

theorem Th22: :: MEASURE1:22

canceled;

theorem Th23: :: MEASURE1:23

for b₁ being set
for b₂ being Field_Subset of b₁ ex b₃ being Function of b₂, ExtREAL st
( b₃ is nonnegative & b₃ . {} = 0. & ( for b₄, b₅ being Element of b₂ st b₄ misses b₅ holds
b₃ . (b₄ \/ b₅) = (b₃ . b₄) + (b₃ . b₅) ) )

proof end;

definition

let c₁ be set ;
let c₂ be Field_Subset of c₁;
mode Measure of c₂ -> Function of a₂, ExtREAL means :Def5: :: MEASURE1:def 5
( a₃ is nonnegative & a₃ . {} = 0. & ( for b₁, b₂ being Element of a₂ st b₁ misses b₂ holds
a₃ . (b₁ \/ b₂) = (a₃ . b₁) + (a₃ . b₂) ) );
existence by Th23;

end;

:: deftheorem Def5 defines Measure MEASURE1:def 5 :

theorem Th24: :: MEASURE1:24

canceled;

theorem Th25: :: MEASURE1:25

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄, b₅ being Element of b₂ st b₄ c= b₅ holds
b₃ . b₄ <=' b₃ . b₅

proof end;

theorem Th26: :: MEASURE1:26

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄, b₅ being Element of b₂ st b₄ c= b₅ & b₃ . b₄ <' +infty holds
b₃ . (b₅ \ b₄) = (b₃ . b₅) - (b₃ . b₄)

proof end;

registration

let c₁ be set ;
cluster non empty cup-closed cap-closed compl-closed Element of bool (bool a₁);
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty cup-closed Subset-Family of c₁;
let c₃, c₄ be Element of c₂;
redefine func \/ as c₃ \/ c₄ -> Element of a₂;
coherence by FINSUB_1:def 1;

end;

definition

let c₁ be set ;
let c₂ be Field_Subset of c₁;
let c₃, c₄ be Element of c₂;
redefine func /\ as c₃ /\ c₄ -> Element of a₂;
coherence by Th19;
redefine func \ as c₃ \ c₄ -> Element of a₂;
coherence by Th20;

end;

theorem Th27: :: MEASURE1:27

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄, b₅ being Element of b₂ holds b₃ . (b₄ \/ b₅) <=' (b₃ . b₄) + (b₃ . b₅)

proof end;

definition

let c₁ be set ;
let c₂ be Field_Subset of c₁;
let c₃ be Measure of c₂;
let c₄ be set ;
pred c₄ is_measurable c₃ means :Def6: :: MEASURE1:def 6
a₄ in a₂;

end;

:: deftheorem Def6 defines is_measurable MEASURE1:def 6 :

theorem Th28: :: MEASURE1:28

canceled;

theorem Th29: :: MEASURE1:29

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂ holds
( {} is_measurable b₃ & b₁ is_measurable b₃ & ( for b₄, b₅ being set st b₄ is_measurable b₃ & b₅ is_measurable b₃ holds
( b₁ \ b₄ is_measurable b₃ & b₄ \/ b₅ is_measurable b₃ & b₄ /\ b₅ is_measurable b₃ ) ) )

proof end;

definition

let c₁ be set ;
let c₂ be Field_Subset of c₁;
let c₃ be Measure of c₂;
mode measure_zero of c₃ -> Element of a₂ means :Def7: :: MEASURE1:def 7
a₃ . a₄ = 0. ;
existence

proof end;

end;

:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :

theorem Th30: :: MEASURE1:30

canceled;

theorem Th31: :: MEASURE1:31

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄ being Element of b₂
for b₅ being measure_zero of b₃ st b₄ c= b₅ holds
b₄ is measure_zero of b₃

proof end;

theorem Th32: :: MEASURE1:32

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄, b₅ being measure_zero of b₃ holds
( b₄ \/ b₅ is measure_zero of b₃ & b₄ /\ b₅ is measure_zero of b₃ & b₄ \ b₅ is measure_zero of b₃ )

proof end;

theorem Th33: :: MEASURE1:33

for b₁ being set
for b₂ being Field_Subset of b₁
for b₃ being Measure of b₂
for b₄ being Element of b₂
for b₅ being measure_zero of b₃ holds
( b₃ . (b₄ \/ b₅) = b₃ . b₄ & b₃ . (b₄ /\ b₅) = 0. & b₃ . (b₄ \ b₅) = b₃ . b₄ )

proof end;

theorem Th34: :: MEASURE1:34

for b₁ being set
for b₂ being Subset of b₁ ex b₃ being Function of NAT , bool b₁ st rng b₃ = {b₂}

proof end;

theorem Th35: :: MEASURE1:35

for b₁ being set ex b₂ being Function of NAT ,{b₁} st
for b₃ being Nat holds b₂ . b₃ = b₁

proof end;

registration

let c₁ be set ;
cluster non empty countable Element of bool (bool a₁);
existence

proof end;

end;

definition

let c₁ be set ;
mode N_Sub_set_fam of a₁ is non empty countable Subset-Family of a₁;

end;

theorem Th36: :: MEASURE1:36

canceled;

theorem Th37: :: MEASURE1:37

canceled;

theorem Th38: :: MEASURE1:38

for b₁ being set
for b₂, b₃, b₄ being Subset of b₁ ex b₅ being Function of NAT , bool b₁ st
( rng b₅ = {b₂,b₃,b₄} & b₅ . 0 = b₂ & b₅ . 1 = b₃ & ( for b₆ being Nat st 1 < b₆ holds
b₅ . b₆ = b₄ ) )

proof end;

theorem Th39: :: MEASURE1:39

for b₁ being set
for b₂, b₃ being Subset of b₁ holds {b₂,b₃,{} } is N_Sub_set_fam of b₁

proof end;

theorem Th40: :: MEASURE1:40

for b₁ being set
for b₂, b₃ being Subset of b₁ ex b₄ being Function of NAT , bool b₁ st
( rng b₄ = {b₂,b₃} & b₄ . 0 = b₂ & ( for b₅ being Nat st 0 < b₅ holds
b₄ . b₅ = b₃ ) )

proof end;

theorem Th41: :: MEASURE1:41

for b₁ being set
for b₂, b₃ being Subset of b₁ holds {b₂,b₃} is N_Sub_set_fam of b₁

proof end;

theorem Th42: :: MEASURE1:42

for b₁ being set
for b₂ being N_Sub_set_fam of b₁ holds b₁ \ b₂ is N_Sub_set_fam of b₁

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
canceled;
attr a₂ is sigma_Field_Subset-like means :Def9: :: MEASURE1:def 9
for b₁ being N_Sub_set_fam of a₁ st b₁ c= a₂ holds
union b₁ in a₂;

end;

:: deftheorem Def8 MEASURE1:def 8 :

:: deftheorem Def9 defines sigma_Field_Subset-like MEASURE1:def 9 :

registration

let c₁ be set ;
cluster non empty compl-closed sigma_Field_Subset-like Element of bool (bool a₁);
existence

proof end;

end;

definition

let c₁ be set ;
mode sigma_Field_Subset of a₁ is non empty compl-closed sigma_Field_Subset-like Subset-Family of a₁;

end;

Lemma28: for b₁ being set
for b₂ being non empty Subset-Family of b₁ st b₂ is sigma_Field_Subset of b₁ holds
b₂ is Field_Subset of b₁

proof end;

theorem Th43: :: MEASURE1:43

canceled;

theorem Th44: :: MEASURE1:44

canceled;

theorem Th45: :: MEASURE1:45

for b₁ being set
for b₂ being sigma_Field_Subset of b₁ holds
( {} in b₂ & b₁ in b₂ )

proof end;

registration

let c₁ be set ;
cluster -> Element of bool (bool a₁);
coherence ;

end;

theorem Th46: :: MEASURE1:46

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃, b₄ being set st b₃ in b₂ & b₄ in b₂ holds
( b₃ \/ b₄ in b₂ & b₃ /\ b₄ in b₂ )

proof end;

theorem Th47: :: MEASURE1:47

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

proof end;

theorem Th48: :: MEASURE1:48

for b₁ being set
for b₂ being sigma_Field_Subset of b₁ holds b₂ = b₁ \ b₂

proof end;

theorem Th49: :: MEASURE1:49

for b₁ being set
for b₂ being non empty Subset-Family of b₁ holds
( ( ( for b₃ being set st b₃ in b₂ holds
b₁ \ b₃ in b₂ ) & ( for b₃ being N_Sub_set_fam of b₁ st b₃ c= b₂ holds
meet b₃ in b₂ ) ) iff b₂ is sigma_Field_Subset of b₁ )

proof end;

registration

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
cluster disjoint_valued M8( NAT ,a₂);
existence

proof end;

end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
mode Sep_Sequence of a₂ is disjoint_valued Function of NAT ,a₂;

end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be Function of NAT ,c₂;
redefine func rng as rng c₃ -> non empty Subset-Family of a₁;
coherence

proof end;

end;

theorem Th50: :: MEASURE1:50

canceled;

theorem Th51: :: MEASURE1:51

canceled;

theorem Th52: :: MEASURE1:52

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Function of NAT ,b₂ holds rng b₃ is N_Sub_set_fam of b₁

proof end;

theorem Th53: :: MEASURE1:53

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being Function of NAT ,b₂ holds union (rng b₃) is Element of b₂

proof end;

theorem Th54: :: MEASURE1:54

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂, ExtREAL st b₄ is nonnegative holds
b₄ * b₃ is nonnegative

proof end;

theorem Th55: :: MEASURE1:55

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

proof end;

theorem Th56: :: MEASURE1:56

for b₁ being set
for b₂ being sigma_Field_Subset of b₁ ex b₃ being Function of b₂, ExtREAL st
for b₄ being Element of b₂ holds
( ( b₄ = {} implies b₃ . b₄ = 0. ) & ( b₄ <> {} implies b₃ . b₄ = +infty ) ) by Th55;

theorem Th57: :: MEASURE1:57

for b₁ being set
for b₂ being sigma_Field_Subset of b₁ ex b₃ being Function of b₂, ExtREAL st
for b₄ being Element of b₂ holds b₃ . b₄ = 0.

proof end;

theorem Th58: :: MEASURE1:58

for b₁ being set
for b₂ being sigma_Field_Subset of b₁ ex b₃ being Function of b₂, ExtREAL st
( b₃ is nonnegative & b₃ . {} = 0. & ( for b₄ being Sep_Sequence of b₂ holds SUM (b₃ * b₄) = b₃ . (union (rng b₄)) ) )

proof end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
canceled;
mode sigma_Measure of c₂ -> Function of a₂, ExtREAL means :Def11: :: MEASURE1:def 11
( a₃ is nonnegative & a₃ . {} = 0. & ( for b₁ being Sep_Sequence of a₂ holds SUM (a₃ * b₁) = a₃ . (union (rng b₁)) ) );
existence by Th58;

end;

:: deftheorem Def10 MEASURE1:def 10 :

:: deftheorem Def11 defines sigma_Measure MEASURE1:def 11 :

registration

let c₁ be set ;
cluster non empty compl-closed sigma_Field_Subset-like -> non empty cup-closed Element of bool (bool a₁);
coherence by Lemma28;

end;

theorem Th59: :: MEASURE1:59

canceled;

theorem Th60: :: MEASURE1:60

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂ holds b₃ is Measure of b₂

proof end;

theorem Th61: :: MEASURE1:61

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Element of b₂ st b₄ misses b₅ holds
b₃ . (b₄ \/ b₅) = (b₃ . b₄) + (b₃ . b₅)

proof end;

theorem Th62: :: MEASURE1:62

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Element of b₂ st b₄ c= b₅ holds
b₃ . b₄ <=' b₃ . b₅

proof end;

theorem Th63: :: MEASURE1:63

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Element of b₂ st b₄ c= b₅ & b₃ . b₄ <' +infty holds
b₃ . (b₅ \ b₄) = (b₃ . b₅) - (b₃ . b₄)

proof end;

theorem Th64: :: MEASURE1:64

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being Element of b₂ holds b₃ . (b₄ \/ b₅) <=' (b₃ . b₄) + (b₃ . b₅)

proof end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
let c₄ be set ;
pred c₄ is_measurable c₃ means :Def12: :: MEASURE1:def 12
a₄ in a₂;

end;

:: deftheorem Def12 defines is_measurable MEASURE1:def 12 :

theorem Th65: :: MEASURE1:65

canceled;

theorem Th66: :: MEASURE1:66

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂ holds
( {} is_measurable b₃ & b₁ is_measurable b₃ & ( for b₄, b₅ being set st b₄ is_measurable b₃ & b₅ is_measurable b₃ holds
( b₁ \ b₄ is_measurable b₃ & b₄ \/ b₅ is_measurable b₃ & b₄ /\ b₅ is_measurable b₃ ) ) )

proof end;

theorem Th67: :: MEASURE1:67

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being N_Sub_set_fam of b₁ st ( for b₅ being set st b₅ in b₄ holds
b₅ is_measurable b₃ ) holds
( union b₄ is_measurable b₃ & meet b₄ is_measurable b₃ )

proof end;

definition

let c₁ be set ;
let c₂ be sigma_Field_Subset of c₁;
let c₃ be sigma_Measure of c₂;
mode measure_zero of c₃ -> Element of a₂ means :Def13: :: MEASURE1:def 13
a₃ . a₄ = 0. ;
existence

proof end;

end;

:: deftheorem Def13 defines measure_zero MEASURE1:def 13 :

theorem Th68: :: MEASURE1:68

canceled;

theorem Th69: :: MEASURE1:69

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Element of b₂
for b₅ being measure_zero of b₃ st b₄ c= b₅ holds
b₄ is measure_zero of b₃

proof end;

theorem Th70: :: MEASURE1:70

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄, b₅ being measure_zero of b₃ holds
( b₄ \/ b₅ is measure_zero of b₃ & b₄ /\ b₅ is measure_zero of b₃ & b₄ \ b₅ is measure_zero of b₃ )

proof end;

theorem Th71: :: MEASURE1:71

for b₁ being set
for b₂ being sigma_Field_Subset of b₁
for b₃ being sigma_Measure of b₂
for b₄ being Element of b₂
for b₅ being measure_zero of b₃ holds
( b₃ . (b₄ \/ b₅) = b₃ . b₄ & b₃ . (b₄ /\ b₅) = 0. & b₃ . (b₄ \ b₅) = b₃ . b₄ )

proof end;